FindProof---0.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : FindProof---0.1
% Problem  : GEO181+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 : n009.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:18 PM UTC 2026

% Result   : Theorem 20.56s 8.09s
% Output   : Proof 20.56s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : GEO181+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04  % Command  : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/5.38  % Computer : n009.cluster.edu
% 0.09/5.38  % Model    : x86_64 x86_64
% 0.09/5.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38  % Memory   : 8046.5625MB
% 0.09/5.38  % OS       : Linux 6.8.0-71-generic
% 0.09/5.38  % CPULimit : 300
% 0.09/5.38  % WCLimit  : 300
% 0.09/5.38  % DateTime : Wed Sep 23 11:19:18 UTC 2026
% 0.09/5.38  % CPUTime  : 
% 0.09/5.38  Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 20.56/8.09  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.56/8.09  % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.56/8.09  fof(sdef10, definition, (spl10 <=> (distinct_points(sk2,sk2))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 20.56/8.09  cnf(p433, plain, (distinct_points(sk2,sk2) | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 20.56/8.09  fof(f0, axiom, ! [X] : ~ distinct_points(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart1)).
% 20.56/8.09  fof(f0_nnf, plain, ! [X] : (~(distinct_points(X,X))), inference(nnf_transformation, [status(thm)], [f0])).
% 20.56/8.09  fof(f0_sk, plain, ! [X] : (~(distinct_points(X,X))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 20.56/8.09  cnf(c0, plain, ~distinct_points(X0,X0), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 20.56/8.09  cnf(p439, plain, ($false | ~spl10), inference(resolution, [status(thm)], [p433, c0])).
% 20.56/8.09  cnf(sct0, plain, (~spl10), inference(avatar_contradiction_clause, [status(thm)], [p439])).
% 20.56/8.09  fof(sdef1, definition, (spl1 <=> (distinct_points(sk2,X0) | distinct_points(X0,sk2))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 20.56/8.09  cnf(p413, plain, (distinct_points(sk2,X0) | distinct_points(X0,sk2) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 20.56/8.09  cnf(p441, plain, (distinct_points(sk2,sk2) | ~spl1), inference(factoring, [status(thm)], [p413])).
% 20.56/8.09  cnf(p450, plain, ($false | ~spl1), inference(resolution, [status(thm)], [p441, c0])).
% 20.56/8.09  cnf(sct1, plain, (~spl1), inference(avatar_contradiction_clause, [status(thm)], [p450])).
% 20.56/8.09  fof(sdef28, definition, (spl28 <=> (apart_point_and_line(sk0,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 20.56/8.09  cnf(p832, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 20.56/8.09  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)).
% 20.56/8.09  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])).
% 20.56/8.09  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])).
% 20.56/8.09  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])).
% 20.56/8.09  fof(f12, conjecture, ! [X,Y,Z] : ( distinct_points(X,Y) => ( apart_point_and_line(Z,line_connecting(X,Y)) => apart_point_and_line(Y,line_connecting(X,Z)) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 20.56/8.09  fof(f12_neg, negated_conjecture, ~(! [X,Y,Z] : ( distinct_points(X,Y) => ( apart_point_and_line(Z,line_connecting(X,Y)) => apart_point_and_line(Y,line_connecting(X,Z)) ) )), inference(negated_conjecture, [status(cth)], [f12])).
% 20.56/8.09  fof(f12_nnf, plain, ? [X,Y,Z] : ((distinct_points(X,Y) & (apart_point_and_line(Z,line_connecting(X,Y)) & ~(apart_point_and_line(Y,line_connecting(X,Z)))))), inference(nnf_transformation, [status(thm)], [f12_neg])).
% 20.56/8.09  fof(f12_sk, plain, (distinct_points(sk0,sk1) & (apart_point_and_line(sk2,line_connecting(sk0,sk1)) & ~(apart_point_and_line(sk1,line_connecting(sk0,sk2))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2])], [f12_nnf])).
% 20.56/8.09  cnf(c14, plain, distinct_points(sk0,sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 20.56/8.09  cnf(p34, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c6, c14])).
% 20.56/8.09  cnf(p885, plain, (distinct_points(sk0,sk0) | ~spl28), inference(resolution, [status(thm)], [p832, p34])).
% 20.56/8.09  cnf(p888, plain, ($false | ~spl28), inference(resolution, [status(thm)], [p885, c0])).
% 20.56/8.09  cnf(sct2, plain, (~spl28), inference(avatar_contradiction_clause, [status(thm)], [p888])).
% 20.56/8.09  fof(sdef30, definition, (spl30 <=> (apart_point_and_line(sk1,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 20.56/8.09  cnf(p834, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | ~spl30), inference(avatar_component_clause, [status(thm)], [sdef30])).
% 20.56/8.09  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])).
% 20.56/8.09  cnf(p61, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [c7, c14])).
% 20.56/8.09  cnf(p889, plain, (distinct_points(sk1,sk1) | ~spl30), inference(resolution, [status(thm)], [p834, p61])).
% 20.56/8.09  cnf(p892, plain, ($false | ~spl30), inference(resolution, [status(thm)], [p889, c0])).
% 20.56/8.09  cnf(sct3, plain, (~spl30), inference(avatar_contradiction_clause, [status(thm)], [p892])).
% 20.56/8.09  fof(sdef32, definition, (spl32 <=> (apart_point_and_line(sk0,line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 20.56/8.09  cnf(p838, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk0)) | ~spl32), inference(avatar_component_clause, [status(thm)], [sdef32])).
% 20.56/8.09  cnf(c15, plain, apart_point_and_line(sk2,line_connecting(sk0,sk1)), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 20.56/8.09  cnf(p54, plain, distinct_points(sk2,sk0), inference(resolution, [status(thm)], [p34, c15])).
% 20.56/8.09  cnf(p81, plain, ~apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c7, p54])).
% 20.56/8.09  cnf(p944, plain, (distinct_points(sk0,sk0) | ~spl32), inference(resolution, [status(thm)], [p838, p81])).
% 20.56/8.09  cnf(p947, plain, ($false | ~spl32), inference(resolution, [status(thm)], [p944, c0])).
% 20.56/8.09  cnf(sct4, plain, (~spl32), inference(avatar_contradiction_clause, [status(thm)], [p947])).
% 20.56/8.09  fof(sdef34, definition, (spl34 <=> (apart_point_and_line(sk0,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 20.56/8.09  cnf(p841, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | ~spl34), inference(avatar_component_clause, [status(thm)], [sdef34])).
% 20.56/8.09  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)).
% 20.56/8.09  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])).
% 20.56/8.09  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])).
% 20.56/8.09  cnf(c3, plain, ~distinct_points(X0,X1) | distinct_points(X0,X2) | distinct_points(X1,X2), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 20.56/8.09  cnf(p55, plain, distinct_points(sk2,X0) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p54, c3])).
% 20.56/8.09  cnf(p57, plain, distinct_points(sk0,sk2), inference(resolution, [status(thm)], [p55, c0])).
% 20.56/8.09  cnf(p60, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p57, c6])).
% 20.56/8.09  cnf(p950, plain, (distinct_points(sk0,sk0) | ~spl34), inference(resolution, [status(thm)], [p841, p60])).
% 20.56/8.09  cnf(p1004, plain, ($false | ~spl34), inference(resolution, [status(thm)], [p950, c0])).
% 20.56/8.09  cnf(sct5, plain, (~spl34), inference(avatar_contradiction_clause, [status(thm)], [p1004])).
% 20.56/8.09  fof(sdef35, definition, (spl35 <=> (apart_point_and_line(sk1,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 20.56/8.09  cnf(p842, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | ~spl35), inference(avatar_component_clause, [status(thm)], [sdef35])).
% 20.56/8.09  cnf(c16, plain, ~apart_point_and_line(sk1,line_connecting(sk0,sk2)), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 20.56/8.09  cnf(p1005, plain, ($false | ~spl35), inference(resolution, [status(thm)], [p842, c16])).
% 20.56/8.09  cnf(sct6, plain, (~spl35), inference(avatar_contradiction_clause, [status(thm)], [p1005])).
% 20.56/8.09  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)).
% 20.56/8.09  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])).
% 20.56/8.09  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])).
% 20.56/8.09  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])).
% 20.56/8.09  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)).
% 20.56/8.09  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])).
% 20.56/8.09  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])).
% 20.56/8.09  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])).
% 20.56/8.09  cnf(p131, plain, distinct_points(sk2,X0) | apart_point_and_line(X0,line_connecting(sk0,sk1)), inference(resolution, [status(thm)], [c11, c15])).
% 20.56/8.09  cnf(p165, plain, distinct_lines(line_connecting(sk0,sk1),X0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1), inference(resolution, [status(thm)], [c12, p131])).
% 20.56/8.09  cnf(p56, plain, ~apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p54, c6])).
% 20.56/8.09  cnf(p411, plain, distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk0)) | distinct_points(sk2,X0) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p165, p56])).
% 20.56/8.09  fof(sdef0, definition, (spl0 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 20.56/8.09  cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [p411, sdef0, sdef1])).
% 20.56/8.09  cnf(p83, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [c7, p57])).
% 20.56/8.09  cnf(p414, plain, distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)) | distinct_points(sk2,X0) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p165, p83])).
% 20.56/8.09  fof(sdef2, definition, (spl2 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 20.56/8.09  cnf(ssp1, plain, (spl1 | spl2), inference(avatar_split_clause, [status(thm)], [p414, sdef1, sdef2])).
% 20.56/8.09  cnf(p84, plain, distinct_points(sk2,sk1), inference(resolution, [status(thm)], [p61, c15])).
% 20.56/8.09  cnf(p86, plain, ~apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p84, c6])).
% 20.56/8.09  cnf(p416, plain, distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk1)) | distinct_points(sk2,X0) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p165, p86])).
% 20.56/8.09  fof(sdef3, definition, (spl3 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 20.56/8.09  cnf(ssp2, plain, (spl1 | spl3), inference(avatar_split_clause, [status(thm)], [p416, sdef1, sdef3])).
% 20.56/8.09  cnf(p85, plain, distinct_points(sk2,X0) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p84, c3])).
% 20.56/8.09  cnf(p88, plain, distinct_points(sk1,sk2), inference(resolution, [status(thm)], [p85, c0])).
% 20.56/8.09  cnf(p93, plain, ~apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p88, c7])).
% 20.56/8.09  cnf(p418, plain, distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk2)) | distinct_points(sk2,X0) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p165, p93])).
% 20.56/8.09  fof(sdef4, definition, (spl4 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 20.56/8.09  cnf(ssp3, plain, (spl1 | spl4), inference(avatar_split_clause, [status(thm)], [p418, sdef1, sdef4])).
% 20.56/8.09  cnf(p59, plain, distinct_points(sk0,X0) | ~apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p55, c6])).
% 20.56/8.09  cnf(p421, plain, distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk2,X1) | distinct_points(sk0,X0) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p165, p59])).
% 20.56/8.09  fof(sdef5, definition, (spl5 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 20.56/8.09  cnf(ssp4, plain, (spl1 | spl5), inference(avatar_split_clause, [status(thm)], [p421, sdef1, sdef5])).
% 20.56/8.09  cnf(p90, plain, distinct_points(sk1,X0) | ~apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p85, c6])).
% 20.56/8.09  cnf(p423, plain, distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk2,X1) | distinct_points(sk1,X0) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p165, p90])).
% 20.56/8.09  fof(sdef6, definition, (spl6 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 20.56/8.09  cnf(ssp5, plain, (spl1 | spl6), inference(avatar_split_clause, [status(thm)], [p423, sdef1, sdef6])).
% 20.56/8.09  cnf(p58, plain, distinct_points(sk0,X0) | distinct_points(sk2,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p55, c3])).
% 20.56/8.09  cnf(p112, plain, distinct_points(sk0,X0) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p58, c0])).
% 20.56/8.09  cnf(p129, plain, distinct_points(sk0,X0) | ~apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p112, c7])).
% 20.56/8.09  cnf(p426, plain, distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(sk2,X1) | distinct_points(sk0,X0) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p165, p129])).
% 20.56/8.09  fof(sdef7, definition, (spl7 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 20.56/8.09  cnf(ssp6, plain, (spl1 | spl7), inference(avatar_split_clause, [status(thm)], [p426, sdef1, sdef7])).
% 20.56/8.09  cnf(p132, plain, distinct_points(sk2,X0) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p131, p34])).
% 20.56/8.09  cnf(p137, plain, distinct_points(X0,sk0) | ~apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p132, c6])).
% 20.56/8.09  cnf(p428, plain, distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk2,X1) | distinct_points(X0,sk0) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p165, p137])).
% 20.56/8.09  fof(sdef8, definition, (spl8 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 20.56/8.09  cnf(ssp7, plain, (spl1 | spl8), inference(avatar_split_clause, [status(thm)], [p428, sdef1, sdef8])).
% 20.56/8.09  cnf(p138, plain, distinct_points(sk2,X0) | ~apart_point_and_line(X1,line_connecting(X0,sk0)) | distinct_points(X1,X0), inference(resolution, [status(thm)], [p132, c6])).
% 20.56/8.09  cnf(p408, plain, distinct_points(sk2,X0) | ~apart_point_and_line(sk2,line_connecting(X0,sk0)), inference(factoring, [status(thm)], [p138])).
% 20.56/8.09  cnf(p431, plain, distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk0)) | distinct_points(sk2,sk2) | distinct_points(sk2,X0), inference(resolution, [status(thm)], [p165, p408])).
% 20.56/8.09  fof(sdef9, definition, (spl9 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk0)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 20.56/8.09  cnf(ssp8, plain, (spl9 | spl10), inference(avatar_split_clause, [status(thm)], [p431, sdef9, sdef10])).
% 20.56/8.09  cnf(p133, plain, distinct_points(sk2,X0) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p131, p61])).
% 20.56/8.09  cnf(p145, plain, distinct_points(X0,sk1) | ~apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p133, c6])).
% 20.56/8.09  cnf(p434, plain, distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk2,X1) | distinct_points(X0,sk1) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p165, p145])).
% 20.56/8.09  fof(sdef11, definition, (spl11 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 20.56/8.09  cnf(ssp9, plain, (spl1 | spl11), inference(avatar_split_clause, [status(thm)], [p434, sdef1, sdef11])).
% 20.56/8.09  cnf(p146, plain, distinct_points(sk2,X0) | ~apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(X1,X0), inference(resolution, [status(thm)], [p133, c6])).
% 20.56/8.09  cnf(p409, plain, distinct_points(sk2,X0) | ~apart_point_and_line(sk2,line_connecting(X0,sk1)), inference(factoring, [status(thm)], [p146])).
% 20.56/8.09  cnf(p437, plain, distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk1)) | distinct_points(sk2,sk2) | distinct_points(sk2,X0), inference(resolution, [status(thm)], [p165, p409])).
% 20.56/8.09  fof(sdef12, definition, (spl12 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk1)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 20.56/8.09  cnf(ssp10, plain, (spl10 | spl12), inference(avatar_split_clause, [status(thm)], [p437, sdef10, sdef12])).
% 20.56/8.09  cnf(p89, plain, distinct_points(sk1,X0) | distinct_points(sk2,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p85, c3])).
% 20.56/8.09  cnf(p151, plain, distinct_points(sk1,X0) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p89, c0])).
% 20.56/8.09  cnf(p170, plain, distinct_points(sk1,X0) | ~apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p151, c7])).
% 20.56/8.09  cnf(p468, plain, distinct_points(sk1,X0) | distinct_points(X1,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(sk2,X1), inference(resolution, [status(thm)], [p170, p165])).
% 20.56/8.09  fof(sdef13, definition, (spl13 <=> (distinct_points(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 20.56/8.09  cnf(ssp11, plain, (spl1 | spl13), inference(avatar_split_clause, [status(thm)], [p468, sdef1, sdef13])).
% 20.56/8.09  cnf(p164, plain, distinct_lines(line_connecting(sk0,sk1),X0) | apart_point_and_line(sk2,X0), inference(resolution, [status(thm)], [c12, c15])).
% 20.56/8.09  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)).
% 20.56/8.09  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])).
% 20.56/8.09  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])).
% 20.56/8.09  cnf(c4, plain, ~distinct_lines(X0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 20.56/8.09  cnf(p172, plain, apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p164, c4])).
% 20.56/8.09  cnf(p474, plain, distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk0),X0) | distinct_points(sk2,sk2), inference(resolution, [status(thm)], [p172, p56])).
% 20.56/8.09  fof(sdef14, definition, (spl14 <=> (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk0),X0))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 20.56/8.09  cnf(ssp12, plain, (spl10 | spl14), inference(avatar_split_clause, [status(thm)], [p474, sdef10, sdef14])).
% 20.56/8.09  cnf(p476, plain, distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X0) | distinct_points(sk2,sk2), inference(resolution, [status(thm)], [p172, p83])).
% 20.56/8.09  fof(sdef15, definition, (spl15 <=> (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X0))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 20.56/8.09  cnf(ssp13, plain, (spl10 | spl15), inference(avatar_split_clause, [status(thm)], [p476, sdef10, sdef15])).
% 20.56/8.09  cnf(p478, plain, distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk1),X0) | distinct_points(sk2,sk2), inference(resolution, [status(thm)], [p172, p86])).
% 20.56/8.09  fof(sdef16, definition, (spl16 <=> (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk1),X0))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 20.56/8.09  cnf(ssp14, plain, (spl10 | spl16), inference(avatar_split_clause, [status(thm)], [p478, sdef10, sdef16])).
% 20.56/8.09  cnf(p480, plain, distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk1,sk2),X0) | distinct_points(sk2,sk2), inference(resolution, [status(thm)], [p172, p93])).
% 20.56/8.09  fof(sdef17, definition, (spl17 <=> (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk1,sk2),X0))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 20.56/8.09  cnf(ssp15, plain, (spl10 | spl17), inference(avatar_split_clause, [status(thm)], [p480, sdef10, sdef17])).
% 20.56/8.09  cnf(p483, plain, distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,X1),X0) | distinct_points(sk0,X1) | distinct_points(sk2,sk2), inference(resolution, [status(thm)], [p172, p59])).
% 20.56/8.09  fof(sdef18, definition, (spl18 <=> (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,X1),X0) | distinct_points(sk0,X1))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 20.56/8.09  cnf(ssp16, plain, (spl10 | spl18), inference(avatar_split_clause, [status(thm)], [p483, sdef10, sdef18])).
% 20.56/8.09  cnf(p485, plain, distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,X1),X0) | distinct_points(sk1,X1) | distinct_points(sk2,sk2), inference(resolution, [status(thm)], [p172, p90])).
% 20.56/8.09  fof(sdef19, definition, (spl19 <=> (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,X1),X0) | distinct_points(sk1,X1))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 20.56/8.09  cnf(ssp17, plain, (spl10 | spl19), inference(avatar_split_clause, [status(thm)], [p485, sdef10, sdef19])).
% 20.56/8.09  cnf(p488, plain, distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(X1,sk2),X0) | distinct_points(sk0,X1) | distinct_points(sk2,sk2), inference(resolution, [status(thm)], [p172, p129])).
% 20.56/8.09  fof(sdef20, definition, (spl20 <=> (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(X1,sk2),X0) | distinct_points(sk0,X1))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 20.56/8.09  cnf(ssp18, plain, (spl10 | spl20), inference(avatar_split_clause, [status(thm)], [p488, sdef10, sdef20])).
% 20.56/8.09  cnf(p490, plain, distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,X1),X0) | distinct_points(X1,sk0) | distinct_points(sk2,sk2), inference(resolution, [status(thm)], [p172, p137])).
% 20.56/8.09  fof(sdef21, definition, (spl21 <=> (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,X1),X0) | distinct_points(X1,sk0))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 20.56/8.09  cnf(ssp19, plain, (spl10 | spl21), inference(avatar_split_clause, [status(thm)], [p490, sdef10, sdef21])).
% 20.56/8.09  cnf(p494, plain, distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,X1),X0) | distinct_points(X1,sk1) | distinct_points(sk2,sk2), inference(resolution, [status(thm)], [p172, p145])).
% 20.56/8.09  fof(sdef22, definition, (spl22 <=> (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,X1),X0) | distinct_points(X1,sk1))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 20.56/8.09  cnf(ssp20, plain, (spl10 | spl22), inference(avatar_split_clause, [status(thm)], [p494, sdef10, sdef22])).
% 20.56/8.09  cnf(p499, plain, distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(X1,sk2),X0) | distinct_points(sk1,X1) | distinct_points(sk2,sk2), inference(resolution, [status(thm)], [p172, p170])).
% 20.56/8.09  fof(sdef23, definition, (spl23 <=> (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(X1,sk2),X0) | distinct_points(sk1,X1))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 20.56/8.09  cnf(ssp21, plain, (spl10 | spl23), inference(avatar_split_clause, [status(thm)], [p499, sdef10, sdef23])).
% 20.56/8.09  cnf(p125, plain, distinct_points(X0,sk2) | distinct_points(sk0,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p112, c3])).
% 20.56/8.09  cnf(p173, plain, distinct_points(X0,sk2) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p125, c0])).
% 20.56/8.09  cnf(p186, plain, distinct_points(X0,sk0) | ~apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p173, c7])).
% 20.56/8.09  cnf(p512, plain, distinct_points(X0,sk0) | distinct_points(X1,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(sk2,X1), inference(resolution, [status(thm)], [p186, p165])).
% 20.56/8.09  fof(sdef24, definition, (spl24 <=> (distinct_points(X0,sk0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 20.56/8.09  cnf(ssp22, plain, (spl1 | spl24), inference(avatar_split_clause, [status(thm)], [p512, sdef1, sdef24])).
% 20.56/8.09  cnf(p514, plain, distinct_points(X0,sk0) | distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(line_connecting(X0,sk2),X1), inference(resolution, [status(thm)], [p186, p172])).
% 20.56/8.09  fof(sdef25, definition, (spl25 <=> (distinct_points(X0,sk0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(line_connecting(X0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 20.56/8.09  cnf(ssp23, plain, (spl10 | spl25), inference(avatar_split_clause, [status(thm)], [p514, sdef10, sdef25])).
% 20.56/8.09  cnf(p143, plain, distinct_points(X0,sk1) | distinct_points(sk2,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p133, c3])).
% 20.56/8.09  cnf(p221, plain, distinct_points(X0,sk1) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p143, c0])).
% 20.56/8.09  cnf(p233, plain, distinct_points(X0,sk1) | ~apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p221, c7])).
% 20.56/8.09  cnf(p518, plain, distinct_points(X0,sk1) | distinct_points(X1,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(sk2,X1), inference(resolution, [status(thm)], [p233, p165])).
% 20.56/8.09  fof(sdef26, definition, (spl26 <=> (distinct_points(X0,sk1) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 20.56/8.09  cnf(ssp24, plain, (spl1 | spl26), inference(avatar_split_clause, [status(thm)], [p518, sdef1, sdef26])).
% 20.56/8.09  cnf(p520, plain, distinct_points(X0,sk1) | distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(line_connecting(X0,sk2),X1), inference(resolution, [status(thm)], [p233, p172])).
% 20.56/8.09  fof(sdef27, definition, (spl27 <=> (distinct_points(X0,sk1) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(line_connecting(X0,sk2),X1))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 20.56/8.09  cnf(ssp25, plain, (spl10 | spl27), inference(avatar_split_clause, [status(thm)], [p520, sdef10, sdef27])).
% 20.56/8.09  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)).
% 20.56/8.09  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])).
% 20.56/8.09  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])).
% 20.56/8.09  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])).
% 20.56/8.09  cnf(p94, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1), inference(resolution, [status(thm)], [c10, c14])).
% 20.56/8.09  cnf(p831, plain, apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0), inference(resolution, [status(thm)], [p94, p164])).
% 20.56/8.09  fof(sdef29, definition, (spl29 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 20.56/8.09  cnf(ssp26, plain, (spl28 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p831, sdef28, sdef29, sdef30])).
% 20.56/8.09  cnf(p835, plain, apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1), inference(resolution, [status(thm)], [p94, p165])).
% 20.56/8.09  fof(sdef31, definition, (spl31 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 20.56/8.09  cnf(ssp27, plain, (spl28 | spl30 | spl31), inference(avatar_split_clause, [status(thm)], [p835, sdef28, sdef30, sdef31])).
% 20.56/8.09  cnf(p412, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk0)) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 20.56/8.09  cnf(p837, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | ~spl0), inference(resolution, [status(thm)], [p94, p412])).
% 20.56/8.09  fof(sdef33, definition, (spl33 <=> (apart_point_and_line(sk1,line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 20.56/8.09  cnf(ssp28, plain, (~spl0 | spl28 | spl30 | spl32 | spl33), inference(avatar_split_clause, [status(thm)], [p837, sdef28, sdef30, sdef32, sdef33])).
% 20.56/8.09  cnf(p415, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 20.56/8.09  cnf(p840, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | ~spl2), inference(resolution, [status(thm)], [p94, p415])).
% 20.56/8.09  cnf(ssp29, plain, (~spl2 | spl28 | spl30 | spl34 | spl35), inference(avatar_split_clause, [status(thm)], [p840, sdef28, sdef30, sdef34, sdef35])).
% 20.56/8.09  cnf(p417, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk1)) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 20.56/8.09  cnf(p843, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | ~spl3), inference(resolution, [status(thm)], [p94, p417])).
% 20.56/8.09  fof(sdef36, definition, (spl36 <=> (apart_point_and_line(sk0,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 20.56/8.09  fof(sdef37, definition, (spl37 <=> (apart_point_and_line(sk1,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 20.56/8.09  cnf(ssp30, plain, (~spl3 | spl28 | spl30 | spl36 | spl37), inference(avatar_split_clause, [status(thm)], [p843, sdef28, sdef30, sdef36, sdef37])).
% 20.56/8.09  cnf(p419, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk2)) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 20.56/8.09  cnf(p846, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk1,sk2)) | ~spl4), inference(resolution, [status(thm)], [p94, p419])).
% 20.56/8.09  fof(sdef38, definition, (spl38 <=> (apart_point_and_line(sk0,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 20.56/8.09  fof(sdef39, definition, (spl39 <=> (apart_point_and_line(sk1,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 20.56/8.09  cnf(ssp31, plain, (~spl4 | spl28 | spl30 | spl38 | spl39), inference(avatar_split_clause, [status(thm)], [p846, sdef28, sdef30, sdef38, sdef39])).
% 20.56/8.09  cnf(p422, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk0,X0) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 20.56/8.09  cnf(p849, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(sk0,X0) | ~spl5), inference(resolution, [status(thm)], [p94, p422])).
% 20.56/8.09  fof(sdef40, definition, (spl40 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 20.56/8.09  cnf(ssp32, plain, (~spl5 | spl28 | spl30 | spl40), inference(avatar_split_clause, [status(thm)], [p849, sdef28, sdef30, sdef40])).
% 20.56/8.09  cnf(p424, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk1,X0) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 20.56/8.09  cnf(p851, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(sk1,X0) | ~spl6), inference(resolution, [status(thm)], [p94, p424])).
% 20.56/8.09  fof(sdef41, definition, (spl41 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 20.56/8.09  cnf(ssp33, plain, (~spl6 | spl28 | spl30 | spl41), inference(avatar_split_clause, [status(thm)], [p851, sdef28, sdef30, sdef41])).
% 20.56/8.09  cnf(p427, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(sk0,X0) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 20.56/8.09  cnf(p853, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk2)) | distinct_points(sk0,X0) | ~spl7), inference(resolution, [status(thm)], [p94, p427])).
% 20.56/8.09  fof(sdef42, definition, (spl42 <=> (apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(sk1,line_connecting(X0,sk2)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 20.56/8.09  cnf(ssp34, plain, (~spl7 | spl28 | spl30 | spl42), inference(avatar_split_clause, [status(thm)], [p853, sdef28, sdef30, sdef42])).
% 20.56/8.09  cnf(p429, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X0,sk0) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 20.56/8.09  cnf(p855, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(X0,sk0) | ~spl8), inference(resolution, [status(thm)], [p94, p429])).
% 20.56/8.09  fof(sdef43, definition, (spl43 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 20.56/8.09  cnf(ssp35, plain, (~spl8 | spl28 | spl30 | spl43), inference(avatar_split_clause, [status(thm)], [p855, sdef28, sdef30, sdef43])).
% 20.56/8.09  cnf(p432, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk0)) | distinct_points(sk2,X0) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 20.56/8.09  cnf(p857, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk0)) | distinct_points(sk2,X0) | ~spl9), inference(resolution, [status(thm)], [p94, p432])).
% 20.56/8.09  fof(sdef44, definition, (spl44 <=> (apart_point_and_line(sk0,line_connecting(X0,sk0)) | apart_point_and_line(sk1,line_connecting(X0,sk0)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 20.56/8.09  cnf(ssp36, plain, (~spl9 | spl28 | spl30 | spl44), inference(avatar_split_clause, [status(thm)], [p857, sdef28, sdef30, sdef44])).
% 20.56/8.09  cnf(p435, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X0,sk1) | ~spl11), inference(avatar_component_clause, [status(thm)], [sdef11])).
% 20.56/8.09  cnf(p859, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(X0,sk1) | ~spl11), inference(resolution, [status(thm)], [p94, p435])).
% 20.56/8.09  fof(sdef45, definition, (spl45 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 20.56/8.09  cnf(ssp37, plain, (~spl11 | spl28 | spl30 | spl45), inference(avatar_split_clause, [status(thm)], [p859, sdef28, sdef30, sdef45])).
% 20.56/8.09  cnf(p438, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk1)) | distinct_points(sk2,X0) | ~spl12), inference(avatar_component_clause, [status(thm)], [sdef12])).
% 20.56/8.09  cnf(p861, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk1)) | distinct_points(sk2,X0) | ~spl12), inference(resolution, [status(thm)], [p94, p438])).
% 20.56/8.09  fof(sdef46, definition, (spl46 <=> (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk1)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 20.56/8.09  cnf(ssp38, plain, (~spl12 | spl28 | spl30 | spl46), inference(avatar_split_clause, [status(thm)], [p861, sdef28, sdef30, sdef46])).
% 20.56/8.09  cnf(p440, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk0),X0) | ~spl0), inference(resolution, [status(thm)], [p412, c4])).
% 20.56/8.09  cnf(p863, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl0), inference(resolution, [status(thm)], [p94, p440])).
% 20.56/8.09  fof(sdef47, definition, (spl47 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 20.56/8.09  cnf(ssp39, plain, (~spl0 | spl32 | spl33 | spl47), inference(avatar_split_clause, [status(thm)], [p863, sdef32, sdef33, sdef47])).
% 20.56/8.09  cnf(p451, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl2), inference(resolution, [status(thm)], [p415, c4])).
% 20.56/8.09  cnf(p865, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl2), inference(resolution, [status(thm)], [p94, p451])).
% 20.56/8.09  cnf(ssp40, plain, (~spl2 | spl34 | spl35 | spl47), inference(avatar_split_clause, [status(thm)], [p865, sdef34, sdef35, sdef47])).
% 20.56/8.09  cnf(p452, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk1),X0) | ~spl3), inference(resolution, [status(thm)], [p417, c4])).
% 20.56/8.09  cnf(p866, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl3), inference(resolution, [status(thm)], [p94, p452])).
% 20.56/8.09  cnf(ssp41, plain, (~spl3 | spl36 | spl37 | spl47), inference(avatar_split_clause, [status(thm)], [p866, sdef36, sdef37, sdef47])).
% 20.56/8.09  cnf(p453, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk1,sk2),X0) | ~spl4), inference(resolution, [status(thm)], [p419, c4])).
% 20.56/8.09  cnf(p867, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk1,sk2)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl4), inference(resolution, [status(thm)], [p94, p453])).
% 20.56/8.09  cnf(ssp42, plain, (~spl4 | spl38 | spl39 | spl47), inference(avatar_split_clause, [status(thm)], [p867, sdef38, sdef39, sdef47])).
% 20.56/8.09  cnf(p469, plain, (distinct_points(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | ~spl13), inference(avatar_component_clause, [status(thm)], [sdef13])).
% 20.56/8.09  cnf(p868, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk2)) | distinct_points(sk1,X0) | ~spl13), inference(resolution, [status(thm)], [p94, p469])).
% 20.56/8.09  fof(sdef48, definition, (spl48 <=> (apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(sk1,line_connecting(X0,sk2)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 20.56/8.09  cnf(ssp43, plain, (~spl13 | spl28 | spl30 | spl48), inference(avatar_split_clause, [status(thm)], [p868, sdef28, sdef30, sdef48])).
% 20.56/8.09  cnf(p870, plain, apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p94, p172])).
% 20.56/8.09  fof(sdef49, definition, (spl49 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 20.56/8.09  cnf(ssp44, plain, (spl28 | spl30 | spl49), inference(avatar_split_clause, [status(thm)], [p870, sdef28, sdef30, sdef49])).
% 20.56/8.09  cnf(p872, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X1), inference(resolution, [status(thm)], [p94, p172])).
% 20.56/8.09  cnf(ssp45, plain, (spl29 | spl47), inference(avatar_split_clause, [status(thm)], [p872, sdef29, sdef47])).
% 20.56/8.09  cnf(p475, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk0),X0) | ~spl14), inference(avatar_component_clause, [status(thm)], [sdef14])).
% 20.56/8.09  cnf(p873, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl14), inference(resolution, [status(thm)], [p94, p475])).
% 20.56/8.09  cnf(ssp46, plain, (~spl14 | spl32 | spl33 | spl47), inference(avatar_split_clause, [status(thm)], [p873, sdef32, sdef33, sdef47])).
% 20.56/8.09  fof(f1, axiom, ! [X] : ~ distinct_lines(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart2)).
% 20.56/8.09  fof(f1_nnf, plain, ! [X] : (~(distinct_lines(X,X))), inference(nnf_transformation, [status(thm)], [f1])).
% 20.56/8.09  fof(f1_sk, plain, ! [X] : (~(distinct_lines(X,X))), inference(skolemisation, [status(esa)], [f1_nnf])).
% 20.56/8.09  cnf(c1, plain, ~distinct_lines(X0,X0), inference(cnf_transformation, [status(esa)], [f1_sk])).
% 20.56/8.09  cnf(p501, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk0)) | ~spl14), inference(resolution, [status(thm)], [p475, c1])).
% 20.56/8.09  cnf(p874, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | ~spl14), inference(resolution, [status(thm)], [p94, p501])).
% 20.56/8.09  cnf(ssp47, plain, (~spl14 | spl28 | spl30 | spl32 | spl33), inference(avatar_split_clause, [status(thm)], [p874, sdef28, sdef30, sdef32, sdef33])).
% 20.56/8.09  cnf(p477, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 20.56/8.09  cnf(p875, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl15), inference(resolution, [status(thm)], [p94, p477])).
% 20.56/8.09  cnf(ssp48, plain, (~spl15 | spl34 | spl35 | spl47), inference(avatar_split_clause, [status(thm)], [p875, sdef34, sdef35, sdef47])).
% 20.56/8.09  cnf(p503, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)) | ~spl15), inference(resolution, [status(thm)], [p477, c1])).
% 20.56/8.09  cnf(p876, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | ~spl15), inference(resolution, [status(thm)], [p94, p503])).
% 20.56/8.09  cnf(ssp49, plain, (~spl15 | spl28 | spl30 | spl34 | spl35), inference(avatar_split_clause, [status(thm)], [p876, sdef28, sdef30, sdef34, sdef35])).
% 20.56/8.09  cnf(p479, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk2,sk1),X0) | ~spl16), inference(avatar_component_clause, [status(thm)], [sdef16])).
% 20.56/8.09  cnf(p877, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl16), inference(resolution, [status(thm)], [p94, p479])).
% 20.56/8.09  cnf(ssp50, plain, (~spl16 | spl36 | spl37 | spl47), inference(avatar_split_clause, [status(thm)], [p877, sdef36, sdef37, sdef47])).
% 20.56/8.09  cnf(p507, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk1)) | ~spl16), inference(resolution, [status(thm)], [p479, c1])).
% 20.56/8.09  cnf(p878, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | ~spl16), inference(resolution, [status(thm)], [p94, p507])).
% 20.56/8.09  cnf(ssp51, plain, (~spl16 | spl28 | spl30 | spl36 | spl37), inference(avatar_split_clause, [status(thm)], [p878, sdef28, sdef30, sdef36, sdef37])).
% 20.56/8.09  cnf(p481, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk1,sk2),X0) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 20.56/8.09  cnf(p879, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk1,sk2)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl17), inference(resolution, [status(thm)], [p94, p481])).
% 20.56/8.09  cnf(ssp52, plain, (~spl17 | spl38 | spl39 | spl47), inference(avatar_split_clause, [status(thm)], [p879, sdef38, sdef39, sdef47])).
% 20.56/8.09  cnf(p509, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk2)) | ~spl17), inference(resolution, [status(thm)], [p481, c1])).
% 20.56/8.09  cnf(p880, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk1,sk2)) | ~spl17), inference(resolution, [status(thm)], [p94, p509])).
% 20.56/8.09  cnf(ssp53, plain, (~spl17 | spl28 | spl30 | spl38 | spl39), inference(avatar_split_clause, [status(thm)], [p880, sdef28, sdef30, sdef38, sdef39])).
% 20.56/8.09  cnf(p513, plain, (distinct_points(X0,sk0) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 20.56/8.09  cnf(p881, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk2)) | distinct_points(X0,sk0) | ~spl24), inference(resolution, [status(thm)], [p94, p513])).
% 20.56/8.09  fof(sdef50, definition, (spl50 <=> (apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(sk1,line_connecting(X0,sk2)) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 20.56/8.09  cnf(ssp54, plain, (~spl24 | spl28 | spl30 | spl50), inference(avatar_split_clause, [status(thm)], [p881, sdef28, sdef30, sdef50])).
% 20.56/8.09  cnf(p519, plain, (distinct_points(X0,sk1) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | ~spl26), inference(avatar_component_clause, [status(thm)], [sdef26])).
% 20.56/8.09  cnf(p883, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk2)) | distinct_points(X0,sk1) | ~spl26), inference(resolution, [status(thm)], [p94, p519])).
% 20.56/8.09  fof(sdef51, definition, (spl51 <=> (apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(sk1,line_connecting(X0,sk2)) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 20.56/8.09  cnf(ssp55, plain, (~spl26 | spl28 | spl30 | spl51), inference(avatar_split_clause, [status(thm)], [p883, sdef28, sdef30, sdef51])).
% 20.56/8.09  cnf(p17, plain, distinct_points(sk0,X0) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [c3, c14])).
% 20.56/8.09  cnf(p95, 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, p17])).
% 20.56/8.09  cnf(p893, 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) | apart_point_and_line(sk2,X0), inference(resolution, [status(thm)], [p95, p164])).
% 20.56/8.09  fof(sdef52, definition, (spl52 <=> (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) | apart_point_and_line(sk2,X0))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 20.56/8.09  cnf(ssp56, plain, (spl30 | spl52), inference(avatar_split_clause, [status(thm)], [p893, sdef30, sdef52])).
% 20.56/8.09  cnf(p895, 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) | apart_point_and_line(X2,X0) | distinct_points(sk2,X2), inference(resolution, [status(thm)], [p95, p165])).
% 20.56/8.09  fof(sdef53, definition, (spl53 <=> (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) | apart_point_and_line(X2,X0) | distinct_points(sk2,X2))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 20.56/8.09  cnf(ssp57, plain, (spl30 | spl53), inference(avatar_split_clause, [status(thm)], [p895, sdef30, sdef53])).
% 20.56/8.09  cnf(p897, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(sk0,X0) | ~spl0), inference(resolution, [status(thm)], [p95, p412])).
% 20.56/8.09  fof(sdef54, definition, (spl54 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 20.56/8.09  cnf(ssp58, plain, (~spl0 | spl30 | spl33 | spl54), inference(avatar_split_clause, [status(thm)], [p897, sdef30, sdef33, sdef54])).
% 20.56/8.09  cnf(p899, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk0,X0) | ~spl2), inference(resolution, [status(thm)], [p95, p415])).
% 20.56/8.09  fof(sdef55, definition, (spl55 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 20.56/8.09  cnf(ssp59, plain, (~spl2 | spl30 | spl35 | spl55), inference(avatar_split_clause, [status(thm)], [p899, sdef30, sdef35, sdef55])).
% 20.56/8.09  cnf(p901, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk0,X0) | ~spl3), inference(resolution, [status(thm)], [p95, p417])).
% 20.56/8.09  fof(sdef56, definition, (spl56 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 20.56/8.09  cnf(ssp60, plain, (~spl3 | spl30 | spl37 | spl56), inference(avatar_split_clause, [status(thm)], [p901, sdef30, sdef37, sdef56])).
% 20.56/8.09  cnf(p903, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk0,X0) | ~spl4), inference(resolution, [status(thm)], [p95, p419])).
% 20.56/8.09  fof(sdef57, definition, (spl57 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 20.56/8.09  cnf(ssp61, plain, (~spl4 | spl30 | spl39 | spl57), inference(avatar_split_clause, [status(thm)], [p903, sdef30, sdef39, sdef57])).
% 20.56/8.09  cnf(p905, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk0,X1) | distinct_points(sk0,X0) | ~spl5), inference(resolution, [status(thm)], [p95, p422])).
% 20.56/8.09  fof(sdef58, definition, (spl58 <=> (apart_point_and_line(sk1,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk0,X1) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 20.56/8.09  cnf(ssp62, plain, (~spl5 | spl30 | spl58), inference(avatar_split_clause, [status(thm)], [p905, sdef30, sdef58])).
% 20.56/8.09  cnf(p907, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk0,X1) | distinct_points(sk1,X0) | ~spl6), inference(resolution, [status(thm)], [p95, p424])).
% 20.56/8.09  fof(sdef59, definition, (spl59 <=> (apart_point_and_line(sk1,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk0,X1) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 20.56/8.09  cnf(ssp63, plain, (~spl6 | spl30 | spl59), inference(avatar_split_clause, [status(thm)], [p907, sdef30, sdef59])).
% 20.56/8.09  cnf(p909, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk0,X1) | distinct_points(sk0,X0) | ~spl7), inference(resolution, [status(thm)], [p95, p427])).
% 20.56/8.09  fof(sdef60, definition, (spl60 <=> (apart_point_and_line(sk1,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk0,X1) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 20.56/8.09  cnf(ssp64, plain, (~spl7 | spl30 | spl60), inference(avatar_split_clause, [status(thm)], [p909, sdef30, sdef60])).
% 20.56/8.09  cnf(p911, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk0,X1) | distinct_points(X0,sk0) | ~spl8), inference(resolution, [status(thm)], [p95, p429])).
% 20.56/8.09  fof(sdef61, definition, (spl61 <=> (apart_point_and_line(sk1,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk0,X1) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 20.56/8.09  cnf(ssp65, plain, (~spl8 | spl30 | spl61), inference(avatar_split_clause, [status(thm)], [p911, sdef30, sdef61])).
% 20.56/8.09  cnf(p913, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk0)) | distinct_points(sk0,X1) | distinct_points(sk2,X0) | ~spl9), inference(resolution, [status(thm)], [p95, p432])).
% 20.56/8.09  fof(sdef62, definition, (spl62 <=> (apart_point_and_line(sk1,line_connecting(X0,sk0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk0)) | distinct_points(sk0,X1) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 20.56/8.09  cnf(ssp66, plain, (~spl9 | spl30 | spl62), inference(avatar_split_clause, [status(thm)], [p913, sdef30, sdef62])).
% 20.56/8.09  cnf(p915, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk0,X1) | distinct_points(X0,sk1) | ~spl11), inference(resolution, [status(thm)], [p95, p435])).
% 20.56/8.09  fof(sdef63, definition, (spl63 <=> (apart_point_and_line(sk1,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk0,X1) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 20.56/8.09  cnf(ssp67, plain, (~spl11 | spl30 | spl63), inference(avatar_split_clause, [status(thm)], [p915, sdef30, sdef63])).
% 20.56/8.09  cnf(p917, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(sk0,X1) | distinct_points(sk2,X0) | ~spl12), inference(resolution, [status(thm)], [p95, p438])).
% 20.56/8.09  fof(sdef64, definition, (spl64 <=> (apart_point_and_line(sk1,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(sk0,X1) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 20.56/8.09  cnf(ssp68, plain, (~spl12 | spl30 | spl64), inference(avatar_split_clause, [status(thm)], [p917, sdef30, sdef64])).
% 20.56/8.09  cnf(p919, 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(line_connecting(sk0,sk1),X0) | ~spl0), inference(resolution, [status(thm)], [p95, p440])).
% 20.56/8.09  fof(sdef65, definition, (spl65 <=> (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(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 20.56/8.09  cnf(ssp69, plain, (~spl0 | spl33 | spl65), inference(avatar_split_clause, [status(thm)], [p919, sdef33, sdef65])).
% 20.56/8.09  cnf(p921, 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(line_connecting(sk0,sk1),X0) | ~spl2), inference(resolution, [status(thm)], [p95, p451])).
% 20.56/8.09  fof(sdef66, definition, (spl66 <=> (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(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 20.56/8.09  cnf(ssp70, plain, (~spl2 | spl35 | spl66), inference(avatar_split_clause, [status(thm)], [p921, sdef35, sdef66])).
% 20.56/8.09  cnf(p923, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl3), inference(resolution, [status(thm)], [p95, p452])).
% 20.56/8.09  fof(sdef67, definition, (spl67 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 20.56/8.09  cnf(ssp71, plain, (~spl3 | spl37 | spl67), inference(avatar_split_clause, [status(thm)], [p923, sdef37, sdef67])).
% 20.56/8.09  cnf(p925, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk1,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl4), inference(resolution, [status(thm)], [p95, p453])).
% 20.56/8.09  fof(sdef68, definition, (spl68 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk1,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 20.56/8.09  cnf(ssp72, plain, (~spl4 | spl39 | spl68), inference(avatar_split_clause, [status(thm)], [p925, sdef39, sdef68])).
% 20.56/8.09  cnf(p927, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk0,X1) | distinct_points(sk1,X0) | ~spl13), inference(resolution, [status(thm)], [p95, p469])).
% 20.56/8.09  fof(sdef69, definition, (spl69 <=> (apart_point_and_line(sk1,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk0,X1) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 20.56/8.09  cnf(ssp73, plain, (~spl13 | spl30 | spl69), inference(avatar_split_clause, [status(thm)], [p927, sdef30, sdef69])).
% 20.56/8.09  cnf(p929, 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) | apart_point_and_line(sk2,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p95, p172])).
% 20.56/8.10  fof(sdef70, definition, (spl70 <=> (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) | apart_point_and_line(sk2,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 20.56/8.10  cnf(ssp74, plain, (spl30 | spl70), inference(avatar_split_clause, [status(thm)], [p929, sdef30, sdef70])).
% 20.56/8.10  cnf(p932, 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(line_connecting(sk0,sk1),X0) | ~spl14), inference(resolution, [status(thm)], [p95, p475])).
% 20.56/8.10  cnf(ssp75, plain, (~spl14 | spl33 | spl65), inference(avatar_split_clause, [status(thm)], [p932, sdef33, sdef65])).
% 20.56/8.10  cnf(p933, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(sk0,X0) | ~spl14), inference(resolution, [status(thm)], [p95, p501])).
% 20.56/8.10  cnf(ssp76, plain, (~spl14 | spl30 | spl33 | spl54), inference(avatar_split_clause, [status(thm)], [p933, sdef30, sdef33, sdef54])).
% 20.56/8.10  cnf(p934, 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(line_connecting(sk0,sk1),X0) | ~spl15), inference(resolution, [status(thm)], [p95, p477])).
% 20.56/8.10  cnf(ssp77, plain, (~spl15 | spl35 | spl66), inference(avatar_split_clause, [status(thm)], [p934, sdef35, sdef66])).
% 20.56/8.10  cnf(p935, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk0,X0) | ~spl15), inference(resolution, [status(thm)], [p95, p503])).
% 20.56/8.10  cnf(ssp78, plain, (~spl15 | spl30 | spl35 | spl55), inference(avatar_split_clause, [status(thm)], [p935, sdef30, sdef35, sdef55])).
% 20.56/8.10  cnf(p936, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl16), inference(resolution, [status(thm)], [p95, p479])).
% 20.56/8.10  cnf(ssp79, plain, (~spl16 | spl37 | spl67), inference(avatar_split_clause, [status(thm)], [p936, sdef37, sdef67])).
% 20.56/8.10  cnf(p937, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk0,X0) | ~spl16), inference(resolution, [status(thm)], [p95, p507])).
% 20.56/8.10  cnf(ssp80, plain, (~spl16 | spl30 | spl37 | spl56), inference(avatar_split_clause, [status(thm)], [p937, sdef30, sdef37, sdef56])).
% 20.56/8.10  cnf(p938, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk1,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl17), inference(resolution, [status(thm)], [p95, p481])).
% 20.56/8.10  cnf(ssp81, plain, (~spl17 | spl39 | spl68), inference(avatar_split_clause, [status(thm)], [p938, sdef39, sdef68])).
% 20.56/8.10  cnf(p939, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk0,X0) | ~spl17), inference(resolution, [status(thm)], [p95, p509])).
% 20.56/8.10  cnf(ssp82, plain, (~spl17 | spl30 | spl39 | spl57), inference(avatar_split_clause, [status(thm)], [p939, sdef30, sdef39, sdef57])).
% 20.56/8.10  cnf(p940, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk0,X1) | distinct_points(X0,sk0) | ~spl24), inference(resolution, [status(thm)], [p95, p513])).
% 20.56/8.10  fof(sdef71, definition, (spl71 <=> (apart_point_and_line(sk1,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk0,X1) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 20.56/8.10  cnf(ssp83, plain, (~spl24 | spl30 | spl71), inference(avatar_split_clause, [status(thm)], [p940, sdef30, sdef71])).
% 20.56/8.10  cnf(p942, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk0,X1) | distinct_points(X0,sk1) | ~spl26), inference(resolution, [status(thm)], [p95, p519])).
% 20.56/8.10  fof(sdef72, definition, (spl72 <=> (apart_point_and_line(sk1,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk0,X1) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 20.56/8.10  cnf(ssp84, plain, (~spl26 | spl30 | spl72), inference(avatar_split_clause, [status(thm)], [p942, sdef30, sdef72])).
% 20.56/8.10  cnf(p18, plain, distinct_points(sk0,X0) | distinct_points(sk1,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p17, c3])).
% 20.56/8.10  cnf(p96, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(sk1,X3) | distinct_points(X2,X3), inference(resolution, [status(thm)], [c10, p18])).
% 20.56/8.10  cnf(p953, plain, apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | apart_point_and_line(sk2,X0), inference(resolution, [status(thm)], [p96, p164])).
% 20.56/8.10  fof(sdef73, definition, (spl73 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | apart_point_and_line(sk2,X0))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 20.56/8.10  cnf(ssp85, plain, (spl28 | spl73), inference(avatar_split_clause, [status(thm)], [p953, sdef28, sdef73])).
% 20.56/8.10  cnf(p955, plain, apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | apart_point_and_line(X3,X0) | distinct_points(sk2,X3), inference(resolution, [status(thm)], [p96, p165])).
% 20.56/8.10  fof(sdef74, definition, (spl74 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | apart_point_and_line(X3,X0) | distinct_points(sk2,X3))), introduced(definition, [new_symbols(naming, [spl74])], [avatar_definition])).
% 20.56/8.10  cnf(ssp86, plain, (spl28 | spl74), inference(avatar_split_clause, [status(thm)], [p955, sdef28, sdef74])).
% 20.56/8.10  cnf(p957, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl0), inference(resolution, [status(thm)], [p96, p412])).
% 20.56/8.10  fof(sdef75, definition, (spl75 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(sk1,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl75])], [avatar_definition])).
% 20.56/8.10  cnf(ssp87, plain, (~spl0 | spl28 | spl32 | spl75), inference(avatar_split_clause, [status(thm)], [p957, sdef28, sdef32, sdef75])).
% 20.56/8.10  cnf(p959, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl2), inference(resolution, [status(thm)], [p96, p415])).
% 20.56/8.10  fof(sdef76, definition, (spl76 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk1,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl76])], [avatar_definition])).
% 20.56/8.10  cnf(ssp88, plain, (~spl2 | spl28 | spl34 | spl76), inference(avatar_split_clause, [status(thm)], [p959, sdef28, sdef34, sdef76])).
% 20.56/8.10  cnf(p961, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl3), inference(resolution, [status(thm)], [p96, p417])).
% 20.56/8.10  fof(sdef77, definition, (spl77 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk1,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl77])], [avatar_definition])).
% 20.56/8.10  cnf(ssp89, plain, (~spl3 | spl28 | spl36 | spl77), inference(avatar_split_clause, [status(thm)], [p961, sdef28, sdef36, sdef77])).
% 20.56/8.10  cnf(p963, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl4), inference(resolution, [status(thm)], [p96, p419])).
% 20.56/8.10  fof(sdef78, definition, (spl78 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk1,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl78])], [avatar_definition])).
% 20.56/8.10  cnf(ssp90, plain, (~spl4 | spl28 | spl38 | spl78), inference(avatar_split_clause, [status(thm)], [p963, sdef28, sdef38, sdef78])).
% 20.56/8.10  cnf(p965, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(sk0,X0) | ~spl5), inference(resolution, [status(thm)], [p96, p422])).
% 20.56/8.10  fof(sdef79, definition, (spl79 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl79])], [avatar_definition])).
% 20.56/8.10  cnf(ssp91, plain, (~spl5 | spl28 | spl79), inference(avatar_split_clause, [status(thm)], [p965, sdef28, sdef79])).
% 20.56/8.10  cnf(p967, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(sk1,X0) | ~spl6), inference(resolution, [status(thm)], [p96, p424])).
% 20.56/8.10  fof(sdef80, definition, (spl80 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl80])], [avatar_definition])).
% 20.56/8.10  cnf(ssp92, plain, (~spl6 | spl28 | spl80), inference(avatar_split_clause, [status(thm)], [p967, sdef28, sdef80])).
% 20.56/8.10  cnf(p969, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(sk0,X0) | ~spl7), inference(resolution, [status(thm)], [p96, p427])).
% 20.56/8.10  fof(sdef81, definition, (spl81 <=> (apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl81])], [avatar_definition])).
% 20.56/8.10  cnf(ssp93, plain, (~spl7 | spl28 | spl81), inference(avatar_split_clause, [status(thm)], [p969, sdef28, sdef81])).
% 20.56/8.10  cnf(p971, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(X0,sk0) | ~spl8), inference(resolution, [status(thm)], [p96, p429])).
% 20.56/8.10  fof(sdef82, definition, (spl82 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl82])], [avatar_definition])).
% 20.56/8.10  cnf(ssp94, plain, (~spl8 | spl28 | spl82), inference(avatar_split_clause, [status(thm)], [p971, sdef28, sdef82])).
% 20.56/8.10  cnf(p973, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk0)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(sk2,X0) | ~spl9), inference(resolution, [status(thm)], [p96, p432])).
% 20.56/8.10  fof(sdef83, definition, (spl83 <=> (apart_point_and_line(sk0,line_connecting(X0,sk0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk0)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl83])], [avatar_definition])).
% 20.56/8.10  cnf(ssp95, plain, (~spl9 | spl28 | spl83), inference(avatar_split_clause, [status(thm)], [p973, sdef28, sdef83])).
% 20.56/8.10  cnf(p975, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(X0,sk1) | ~spl11), inference(resolution, [status(thm)], [p96, p435])).
% 20.56/8.10  fof(sdef84, definition, (spl84 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl84])], [avatar_definition])).
% 20.56/8.10  cnf(ssp96, plain, (~spl11 | spl28 | spl84), inference(avatar_split_clause, [status(thm)], [p975, sdef28, sdef84])).
% 20.56/8.10  cnf(p977, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(sk2,X0) | ~spl12), inference(resolution, [status(thm)], [p96, p438])).
% 20.56/8.10  fof(sdef85, definition, (spl85 <=> (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl85])], [avatar_definition])).
% 20.56/8.10  cnf(ssp97, plain, (~spl12 | spl28 | spl85), inference(avatar_split_clause, [status(thm)], [p977, sdef28, sdef85])).
% 20.56/8.10  cnf(p979, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl0), inference(resolution, [status(thm)], [p96, p440])).
% 20.56/8.10  fof(sdef86, definition, (spl86 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl86])], [avatar_definition])).
% 20.56/8.10  cnf(ssp98, plain, (~spl0 | spl32 | spl86), inference(avatar_split_clause, [status(thm)], [p979, sdef32, sdef86])).
% 20.56/8.10  cnf(p981, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl2), inference(resolution, [status(thm)], [p96, p451])).
% 20.56/8.10  fof(sdef87, definition, (spl87 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl87])], [avatar_definition])).
% 20.56/8.10  cnf(ssp99, plain, (~spl2 | spl34 | spl87), inference(avatar_split_clause, [status(thm)], [p981, sdef34, sdef87])).
% 20.56/8.10  cnf(p983, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl3), inference(resolution, [status(thm)], [p96, p452])).
% 20.56/8.10  fof(sdef88, definition, (spl88 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl88])], [avatar_definition])).
% 20.56/8.10  cnf(ssp100, plain, (~spl3 | spl36 | spl88), inference(avatar_split_clause, [status(thm)], [p983, sdef36, sdef88])).
% 20.56/8.10  cnf(p985, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk1,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl4), inference(resolution, [status(thm)], [p96, p453])).
% 20.56/8.10  fof(sdef89, definition, (spl89 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk1,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl89])], [avatar_definition])).
% 20.56/8.10  cnf(ssp101, plain, (~spl4 | spl38 | spl89), inference(avatar_split_clause, [status(thm)], [p985, sdef38, sdef89])).
% 20.56/8.10  cnf(p987, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(sk1,X0) | ~spl13), inference(resolution, [status(thm)], [p96, p469])).
% 20.56/8.10  fof(sdef90, definition, (spl90 <=> (apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl90])], [avatar_definition])).
% 20.56/8.10  cnf(ssp102, plain, (~spl13 | spl28 | spl90), inference(avatar_split_clause, [status(thm)], [p987, sdef28, sdef90])).
% 20.56/8.10  cnf(p989, plain, apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | apart_point_and_line(sk2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p96, p172])).
% 20.56/8.10  fof(sdef91, definition, (spl91 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | apart_point_and_line(sk2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl91])], [avatar_definition])).
% 20.56/8.10  cnf(ssp103, plain, (spl28 | spl91), inference(avatar_split_clause, [status(thm)], [p989, sdef28, sdef91])).
% 20.56/8.10  cnf(p992, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl14), inference(resolution, [status(thm)], [p96, p475])).
% 20.56/8.10  cnf(ssp104, plain, (~spl14 | spl32 | spl86), inference(avatar_split_clause, [status(thm)], [p992, sdef32, sdef86])).
% 20.56/8.10  cnf(p993, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl14), inference(resolution, [status(thm)], [p96, p501])).
% 20.56/8.10  cnf(ssp105, plain, (~spl14 | spl28 | spl32 | spl75), inference(avatar_split_clause, [status(thm)], [p993, sdef28, sdef32, sdef75])).
% 20.56/8.10  cnf(p994, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl15), inference(resolution, [status(thm)], [p96, p477])).
% 20.56/8.10  cnf(ssp106, plain, (~spl15 | spl34 | spl87), inference(avatar_split_clause, [status(thm)], [p994, sdef34, sdef87])).
% 20.56/8.10  cnf(p995, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl15), inference(resolution, [status(thm)], [p96, p503])).
% 20.56/8.10  cnf(ssp107, plain, (~spl15 | spl28 | spl34 | spl76), inference(avatar_split_clause, [status(thm)], [p995, sdef28, sdef34, sdef76])).
% 20.56/8.10  cnf(p996, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl16), inference(resolution, [status(thm)], [p96, p479])).
% 20.56/8.10  cnf(ssp108, plain, (~spl16 | spl36 | spl88), inference(avatar_split_clause, [status(thm)], [p996, sdef36, sdef88])).
% 20.56/8.10  cnf(p997, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl16), inference(resolution, [status(thm)], [p96, p507])).
% 20.56/8.10  cnf(ssp109, plain, (~spl16 | spl28 | spl36 | spl77), inference(avatar_split_clause, [status(thm)], [p997, sdef28, sdef36, sdef77])).
% 20.56/8.10  cnf(p998, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk1,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl17), inference(resolution, [status(thm)], [p96, p481])).
% 20.56/8.10  cnf(ssp110, plain, (~spl17 | spl38 | spl89), inference(avatar_split_clause, [status(thm)], [p998, sdef38, sdef89])).
% 20.56/8.10  cnf(p999, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl17), inference(resolution, [status(thm)], [p96, p509])).
% 20.56/8.10  cnf(ssp111, plain, (~spl17 | spl28 | spl38 | spl78), inference(avatar_split_clause, [status(thm)], [p999, sdef28, sdef38, sdef78])).
% 20.56/8.10  cnf(p1000, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(X0,sk0) | ~spl24), inference(resolution, [status(thm)], [p96, p513])).
% 20.56/8.10  fof(sdef92, definition, (spl92 <=> (apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl92])], [avatar_definition])).
% 20.56/8.10  cnf(ssp112, plain, (~spl24 | spl28 | spl92), inference(avatar_split_clause, [status(thm)], [p1000, sdef28, sdef92])).
% 20.56/8.10  cnf(p1002, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(X0,sk1) | ~spl26), inference(resolution, [status(thm)], [p96, p519])).
% 20.56/8.10  fof(sdef93, definition, (spl93 <=> (apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | distinct_points(sk1,X2) | distinct_points(X1,X2) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl93])], [avatar_definition])).
% 20.56/8.10  cnf(ssp113, plain, (~spl26 | spl28 | spl93), inference(avatar_split_clause, [status(thm)], [p1002, sdef28, sdef93])).
% 20.56/8.10  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, sct0, sct1, sct2, sct3, sct4, sct5, sct6])).
% 20.56/8.10  % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------