FindProof---0.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : FindProof---0.1
% Problem  : GEO189+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300

% Computer : n011.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:22 PM UTC 2026

% Result   : Theorem 9.87s 3.40s
% Output   : Proof 9.87s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : GEO189+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03  % Command  : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.37  % Computer : n011.cluster.edu
% 0.10/0.37  % Model    : x86_64 x86_64
% 0.10/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37  % Memory   : 8046.5625MB
% 0.10/0.37  % OS       : Linux 6.8.0-71-generic
% 0.10/0.37  % CPULimit : 300
% 0.10/0.37  % WCLimit  : 300
% 0.10/0.37  % DateTime : Wed Sep 23 11:22:12 UTC 2026
% 0.10/0.37  % CPUTime  : 
% 0.10/0.37  Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 9.87/3.40  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.87/3.40  % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.87/3.40  fof(sdef8, definition, (spl8 <=> (distinct_points(sk1,sk1))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 9.87/3.40  cnf(p467, plain, (distinct_points(sk1,sk1) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 9.87/3.40  fof(f0, axiom, ! [X] : ~ distinct_points(X,X), file('/export/starexec/sandbox/benchmark/theBenchmark.p', apart1)).
% 9.87/3.40  fof(f0_nnf, plain, ! [X] : (~(distinct_points(X,X))), inference(nnf_transformation, [status(thm)], [f0])).
% 9.87/3.40  fof(f0_sk, plain, ! [X] : (~(distinct_points(X,X))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 9.87/3.40  cnf(c0, plain, ~distinct_points(X0,X0), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 9.87/3.40  cnf(p484, plain, ($false | ~spl8), inference(resolution, [status(thm)], [p467, c0])).
% 9.87/3.40  cnf(sct0, plain, (~spl8), inference(avatar_contradiction_clause, [status(thm)], [p484])).
% 9.87/3.40  fof(sdef1, definition, (spl1 <=> (distinct_points(sk1,X0) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 9.87/3.40  cnf(p452, plain, (distinct_points(sk1,X0) | distinct_points(X0,sk1) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 9.87/3.40  cnf(p486, plain, (distinct_points(sk1,sk1) | ~spl1), inference(factoring, [status(thm)], [p452])).
% 9.87/3.40  cnf(p495, plain, ($false | ~spl1), inference(resolution, [status(thm)], [p486, c0])).
% 9.87/3.40  cnf(sct1, plain, (~spl1), inference(avatar_contradiction_clause, [status(thm)], [p495])).
% 9.87/3.40  fof(sdef32, definition, (spl32 <=> (distinct_points(sk0,sk0))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 9.87/3.40  cnf(p871, plain, (distinct_points(sk0,sk0) | ~spl32), inference(avatar_component_clause, [status(thm)], [sdef32])).
% 9.87/3.40  cnf(p883, plain, ($false | ~spl32), inference(resolution, [status(thm)], [p871, c0])).
% 9.87/3.40  cnf(sct2, plain, (~spl32), inference(avatar_contradiction_clause, [status(thm)], [p883])).
% 9.87/3.40  fof(sdef36, definition, (spl36 <=> (distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 9.87/3.40  cnf(p926, plain, (distinct_points(sk2,X0) | ~spl36), inference(avatar_component_clause, [status(thm)], [sdef36])).
% 9.87/3.40  cnf(p938, plain, ($false | ~spl36), inference(resolution, [status(thm)], [p926, c0])).
% 9.87/3.40  cnf(sct3, plain, (~spl36), inference(avatar_contradiction_clause, [status(thm)], [p938])).
% 9.87/3.40  fof(sdef42, definition, (spl42 <=> (apart_point_and_line(sk1,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 9.87/3.40  cnf(p1033, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk2)) | ~spl42), inference(avatar_component_clause, [status(thm)], [sdef42])).
% 9.87/3.40  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/sandbox/benchmark/theBenchmark.p', con1)).
% 9.87/3.40  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])).
% 9.87/3.40  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])).
% 9.87/3.40  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])).
% 9.87/3.40  fof(f12, conjecture, ! [X,Y,Z] : ( ( distinct_points(X,Y) & distinct_points(X,Z) & distinct_points(Y,Z) & ~ apart_point_and_line(Z,line_connecting(X,Y)) ) => ~ apart_point_and_line(Y,line_connecting(X,Z)) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 9.87/3.40  fof(f12_neg, negated_conjecture, ~(! [X,Y,Z] : ( ( distinct_points(X,Y) & distinct_points(X,Z) & distinct_points(Y,Z) & ~ apart_point_and_line(Z,line_connecting(X,Y)) ) => ~ apart_point_and_line(Y,line_connecting(X,Z)) )), inference(negated_conjecture, [status(cth)], [f12])).
% 9.87/3.40  fof(f12_nnf, plain, ? [X,Y,Z] : (((((distinct_points(X,Y) & distinct_points(X,Z)) & distinct_points(Y,Z)) & ~(apart_point_and_line(Z,line_connecting(X,Y)))) & apart_point_and_line(Y,line_connecting(X,Z)))), inference(nnf_transformation, [status(thm)], [f12_neg])).
% 9.87/3.40  fof(f12_sk, plain, ((((distinct_points(sk0,sk1) & distinct_points(sk0,sk2)) & distinct_points(sk1,sk2)) & ~(apart_point_and_line(sk2,line_connecting(sk0,sk1)))) & apart_point_and_line(sk1,line_connecting(sk0,sk2))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2])], [f12_nnf])).
% 9.87/3.40  cnf(c16, plain, distinct_points(sk1,sk2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 9.87/3.40  cnf(p47, plain, ~apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [c6, c16])).
% 9.87/3.40  cnf(p1045, plain, (distinct_points(sk1,sk1) | ~spl42), inference(resolution, [status(thm)], [p1033, p47])).
% 9.87/3.40  cnf(p1048, plain, ($false | ~spl42), inference(resolution, [status(thm)], [p1045, c0])).
% 9.87/3.40  cnf(sct4, plain, (~spl42), inference(avatar_contradiction_clause, [status(thm)], [p1048])).
% 9.87/3.40  fof(sdef43, definition, (spl43 <=> (apart_point_and_line(sk0,line_connecting(sk1,sk0)))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 9.87/3.40  cnf(p1035, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk0)) | ~spl43), inference(avatar_component_clause, [status(thm)], [sdef43])).
% 9.87/3.40  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])).
% 9.87/3.40  fof(f3, axiom, ! [X,Y,Z] : ( distinct_points(X,Y) => ( distinct_points(X,Z) | distinct_points(Y,Z) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', apart4)).
% 9.87/3.40  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])).
% 9.87/3.40  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])).
% 9.87/3.40  cnf(c3, plain, ~distinct_points(X0,X1) | distinct_points(X0,X2) | distinct_points(X1,X2), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 9.87/3.40  cnf(c14, plain, distinct_points(sk0,sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 9.87/3.40  cnf(p19, plain, distinct_points(sk0,X0) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [c3, c14])).
% 9.87/3.40  cnf(p22, plain, distinct_points(sk0,X0) | distinct_points(sk1,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p19, c3])).
% 9.87/3.40  cnf(p25, plain, distinct_points(sk0,X0) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p22, c0])).
% 9.87/3.40  cnf(p29, plain, distinct_points(X0,sk1) | distinct_points(sk0,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p25, c3])).
% 9.87/3.40  cnf(p40, plain, distinct_points(X0,sk1) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p29, c0])).
% 9.87/3.40  cnf(p43, plain, distinct_points(sk1,sk0), inference(resolution, [status(thm)], [p40, c0])).
% 9.87/3.40  cnf(p96, plain, ~apart_point_and_line(X0,line_connecting(sk1,sk0)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c7, p43])).
% 9.87/3.40  cnf(p1049, plain, (distinct_points(sk0,sk0) | ~spl43), inference(resolution, [status(thm)], [p1035, p96])).
% 9.87/3.40  cnf(p1191, plain, ($false | ~spl43), inference(resolution, [status(thm)], [p1049, c0])).
% 9.87/3.40  cnf(sct5, plain, (~spl43), inference(avatar_contradiction_clause, [status(thm)], [p1191])).
% 9.87/3.40  fof(sdef44, definition, (spl44 <=> (apart_point_and_line(sk1,line_connecting(sk1,sk0)))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 9.87/3.40  cnf(p1036, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk0)) | ~spl44), inference(avatar_component_clause, [status(thm)], [sdef44])).
% 9.87/3.40  cnf(p70, plain, ~apart_point_and_line(X0,line_connecting(sk1,sk0)) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [c6, p43])).
% 9.87/3.40  cnf(p1192, plain, (distinct_points(sk1,sk1) | ~spl44), inference(resolution, [status(thm)], [p1036, p70])).
% 9.87/3.40  cnf(p1195, plain, ($false | ~spl44), inference(resolution, [status(thm)], [p1192, c0])).
% 9.87/3.40  cnf(sct6, plain, (~spl44), inference(avatar_contradiction_clause, [status(thm)], [p1195])).
% 9.87/3.40  fof(sdef46, definition, (spl46 <=> (apart_point_and_line(sk1,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 9.87/3.40  cnf(p1039, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | ~spl46), inference(avatar_component_clause, [status(thm)], [sdef46])).
% 9.87/3.40  cnf(p21, plain, distinct_points(sk1,X0) | distinct_points(sk2,X0), inference(resolution, [status(thm)], [c3, c16])).
% 9.87/3.40  cnf(p24, plain, distinct_points(sk1,X0) | distinct_points(sk2,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p21, c3])).
% 9.87/3.40  cnf(p35, plain, distinct_points(sk1,X0) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p24, c0])).
% 9.87/3.40  cnf(p39, plain, distinct_points(X0,sk2) | distinct_points(sk1,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p35, c3])).
% 9.87/3.40  cnf(p112, plain, distinct_points(X0,sk2) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p39, c0])).
% 9.87/3.40  cnf(p121, plain, distinct_points(sk2,sk1), inference(resolution, [status(thm)], [p112, c0])).
% 9.87/3.40  cnf(p126, plain, ~apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p121, c7])).
% 9.87/3.40  cnf(p1205, plain, (distinct_points(sk1,sk1) | ~spl46), inference(resolution, [status(thm)], [p1039, p126])).
% 9.87/3.40  cnf(p1208, plain, ($false | ~spl46), inference(resolution, [status(thm)], [p1205, c0])).
% 9.87/3.40  cnf(sct7, plain, (~spl46), inference(avatar_contradiction_clause, [status(thm)], [p1208])).
% 9.87/3.40  fof(sdef47, definition, (spl47 <=> (apart_point_and_line(sk0,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 9.87/3.40  cnf(p1053, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | ~spl47), inference(avatar_component_clause, [status(thm)], [sdef47])).
% 9.87/3.40  cnf(c15, plain, distinct_points(sk0,sk2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 9.87/3.40  cnf(p46, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c6, c15])).
% 9.87/3.40  cnf(p1209, plain, (distinct_points(sk0,sk0) | ~spl47), inference(resolution, [status(thm)], [p1053, p46])).
% 9.87/3.40  cnf(p1212, plain, ($false | ~spl47), inference(resolution, [status(thm)], [p1209, c0])).
% 9.87/3.40  cnf(sct8, plain, (~spl47), inference(avatar_contradiction_clause, [status(thm)], [p1212])).
% 9.87/3.40  fof(sdef49, definition, (spl49 <=> (apart_point_and_line(sk2,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 9.87/3.40  cnf(p1055, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | ~spl49), inference(avatar_component_clause, [status(thm)], [sdef49])).
% 9.87/3.40  cnf(p72, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [c7, c15])).
% 9.87/3.40  cnf(p1222, plain, (distinct_points(sk2,sk2) | ~spl49), inference(resolution, [status(thm)], [p1055, p72])).
% 9.87/3.40  cnf(p1225, plain, ($false | ~spl49), inference(resolution, [status(thm)], [p1222, c0])).
% 9.87/3.40  cnf(sct9, plain, (~spl49), inference(avatar_contradiction_clause, [status(thm)], [p1225])).
% 9.87/3.40  fof(sdef51, definition, (spl51 <=> (apart_point_and_line(sk2,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 9.87/3.40  cnf(p1059, plain, (apart_point_and_line(sk2,line_connecting(sk1,sk2)) | ~spl51), inference(avatar_component_clause, [status(thm)], [sdef51])).
% 9.87/3.40  cnf(p73, plain, ~apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [c7, c16])).
% 9.87/3.40  cnf(p1226, plain, (distinct_points(sk2,sk2) | ~spl51), inference(resolution, [status(thm)], [p1059, p73])).
% 9.87/3.40  cnf(p1229, plain, ($false | ~spl51), inference(resolution, [status(thm)], [p1226, c0])).
% 9.87/3.40  cnf(sct10, plain, (~spl51), inference(avatar_contradiction_clause, [status(thm)], [p1229])).
% 9.87/3.40  fof(sdef53, definition, (spl53 <=> (apart_point_and_line(sk0,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 9.87/3.40  cnf(p1063, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | ~spl53), inference(avatar_component_clause, [status(thm)], [sdef53])).
% 9.87/3.40  cnf(p45, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c6, c14])).
% 9.87/3.40  cnf(p1369, plain, (distinct_points(sk0,sk0) | ~spl53), inference(resolution, [status(thm)], [p1063, p45])).
% 9.87/3.40  cnf(p1372, plain, ($false | ~spl53), inference(resolution, [status(thm)], [p1369, c0])).
% 9.87/3.40  cnf(sct11, plain, (~spl53), inference(avatar_contradiction_clause, [status(thm)], [p1372])).
% 9.87/3.40  fof(sdef54, definition, (spl54 <=> (apart_point_and_line(sk2,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 9.87/3.40  cnf(p1064, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | ~spl54), inference(avatar_component_clause, [status(thm)], [sdef54])).
% 9.87/3.40  cnf(c17, plain, ~apart_point_and_line(sk2,line_connecting(sk0,sk1)), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 9.87/3.40  cnf(p1373, plain, ($false | ~spl54), inference(resolution, [status(thm)], [p1064, c17])).
% 9.87/3.40  cnf(sct12, plain, (~spl54), inference(avatar_contradiction_clause, [status(thm)], [p1373])).
% 9.87/3.40  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/sandbox/benchmark/theBenchmark.p', ceq2)).
% 9.87/3.40  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])).
% 9.87/3.40  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])).
% 9.87/3.40  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])).
% 9.87/3.40  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/sandbox/benchmark/theBenchmark.p', ceq1)).
% 9.87/3.40  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])).
% 9.87/3.40  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])).
% 9.87/3.40  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])).
% 9.87/3.40  cnf(c18, plain, apart_point_and_line(sk1,line_connecting(sk0,sk2)), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 9.87/3.40  cnf(p174, plain, distinct_points(sk1,X0) | apart_point_and_line(X0,line_connecting(sk0,sk2)), inference(resolution, [status(thm)], [c11, c18])).
% 9.87/3.40  cnf(p205, plain, distinct_lines(line_connecting(sk0,sk2),X0) | apart_point_and_line(X1,X0) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [c12, p174])).
% 9.87/3.40  cnf(p450, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,sk2)) | distinct_points(sk1,X0) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p205, p47])).
% 9.87/3.40  fof(sdef0, definition, (spl0 <=> (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 9.87/3.40  cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [p450, sdef0, sdef1])).
% 9.87/3.40  cnf(p453, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,sk0)) | distinct_points(sk1,X0) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p205, p70])).
% 9.87/3.40  fof(sdef2, definition, (spl2 <=> (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,sk0)))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 9.87/3.40  cnf(ssp1, plain, (spl1 | spl2), inference(avatar_split_clause, [status(thm)], [p453, sdef1, sdef2])).
% 9.87/3.40  cnf(p71, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [c7, c14])).
% 9.87/3.40  cnf(p455, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(sk0,sk1)) | distinct_points(sk1,X0) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p205, p71])).
% 9.87/3.40  fof(sdef3, definition, (spl3 <=> (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 9.87/3.40  cnf(ssp2, plain, (spl1 | spl3), inference(avatar_split_clause, [status(thm)], [p455, sdef1, sdef3])).
% 9.87/3.40  cnf(p457, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(sk2,sk1)) | distinct_points(sk1,X0) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p205, p126])).
% 9.87/3.40  fof(sdef4, definition, (spl4 <=> (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 9.87/3.40  cnf(ssp3, plain, (spl1 | spl4), inference(avatar_split_clause, [status(thm)], [p457, sdef1, sdef4])).
% 9.87/3.40  cnf(p48, plain, ~apart_point_and_line(X0,line_connecting(sk1,X1)) | distinct_points(X0,sk1) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [c6, p19])).
% 9.87/3.40  cnf(p460, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | distinct_points(sk1,X1) | distinct_points(X1,sk1) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p205, p48])).
% 9.87/3.40  fof(sdef5, definition, (spl5 <=> (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 9.87/3.40  cnf(ssp4, plain, (spl1 | spl5), inference(avatar_split_clause, [status(thm)], [p460, sdef1, sdef5])).
% 9.87/3.40  cnf(p64, plain, ~apart_point_and_line(X0,line_connecting(sk1,X1)) | distinct_points(X0,sk1) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [c6, p35])).
% 9.87/3.40  cnf(p462, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | distinct_points(sk1,X1) | distinct_points(X1,sk1) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p205, p64])).
% 9.87/3.40  fof(sdef6, definition, (spl6 <=> (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | distinct_points(X0,sk2))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 9.87/3.40  cnf(ssp5, plain, (spl1 | spl6), inference(avatar_split_clause, [status(thm)], [p462, sdef1, sdef6])).
% 9.87/3.40  cnf(p65, plain, ~apart_point_and_line(X0,line_connecting(X1,sk2)) | distinct_points(X0,X1) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [c6, p35])).
% 9.87/3.40  cnf(p305, plain, ~apart_point_and_line(sk1,line_connecting(X0,sk2)) | distinct_points(sk1,X0), inference(factoring, [status(thm)], [p65])).
% 9.87/3.40  cnf(p465, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk2)) | distinct_points(sk1,sk1) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p205, p305])).
% 9.87/3.40  fof(sdef7, definition, (spl7 <=> (distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk2)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 9.87/3.40  cnf(ssp6, plain, (spl7 | spl8), inference(avatar_split_clause, [status(thm)], [p465, sdef7, sdef8])).
% 9.87/3.40  cnf(p76, plain, ~apart_point_and_line(X0,line_connecting(sk2,X1)) | distinct_points(X0,X1) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [c7, p21])).
% 9.87/3.40  cnf(p342, plain, ~apart_point_and_line(sk1,line_connecting(sk2,X0)) | distinct_points(sk1,X0), inference(factoring, [status(thm)], [p76])).
% 9.87/3.40  cnf(p469, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(sk2,X0)) | distinct_points(sk1,sk1) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p205, p342])).
% 9.87/3.40  fof(sdef9, definition, (spl9 <=> (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk2,X0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 9.87/3.40  cnf(ssp7, plain, (spl8 | spl9), inference(avatar_split_clause, [status(thm)], [p469, sdef8, sdef9])).
% 9.87/3.40  cnf(p81, plain, ~apart_point_and_line(X0,line_connecting(X1,sk1)) | distinct_points(X0,sk1) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [c7, p25])).
% 9.87/3.40  cnf(p472, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk1)) | distinct_points(sk1,X1) | distinct_points(X1,sk1) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p205, p81])).
% 9.87/3.40  fof(sdef10, definition, (spl10 <=> (distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk1)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 9.87/3.40  cnf(ssp8, plain, (spl1 | spl10), inference(avatar_split_clause, [status(thm)], [p472, sdef1, sdef10])).
% 9.87/3.40  cnf(p95, plain, ~apart_point_and_line(X0,line_connecting(X1,sk1)) | distinct_points(X0,sk1) | distinct_points(X1,sk0), inference(resolution, [status(thm)], [c7, p40])).
% 9.87/3.40  cnf(p474, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk1)) | distinct_points(sk1,X1) | distinct_points(X1,sk1) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p205, p95])).
% 9.87/3.40  fof(sdef11, definition, (spl11 <=> (distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk1)) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 9.87/3.40  cnf(ssp9, plain, (spl1 | spl11), inference(avatar_split_clause, [status(thm)], [p474, sdef1, sdef11])).
% 9.87/3.40  cnf(p44, plain, distinct_points(X0,sk0) | distinct_points(X0,X1) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [p40, c3])).
% 9.87/3.40  cnf(p157, plain, distinct_points(X0,sk0) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p44, c0])).
% 9.87/3.40  cnf(p169, plain, distinct_points(sk1,X0) | ~apart_point_and_line(X1,line_connecting(X0,sk0)) | distinct_points(X1,X0), inference(resolution, [status(thm)], [p157, c6])).
% 9.87/3.40  cnf(p393, plain, distinct_points(sk1,X0) | ~apart_point_and_line(sk1,line_connecting(X0,sk0)), inference(factoring, [status(thm)], [p169])).
% 9.87/3.40  cnf(p478, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk0)) | distinct_points(sk1,sk1) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p205, p393])).
% 9.87/3.40  fof(sdef12, definition, (spl12 <=> (distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 9.87/3.40  cnf(ssp10, plain, (spl8 | spl12), inference(avatar_split_clause, [status(thm)], [p478, sdef8, sdef12])).
% 9.87/3.40  cnf(p170, plain, distinct_points(X0,sk0) | ~apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(X1,sk1), inference(resolution, [status(thm)], [p157, c6])).
% 9.87/3.40  cnf(p480, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | distinct_points(sk1,X1) | distinct_points(X0,sk0) | distinct_points(X1,sk1), inference(resolution, [status(thm)], [p205, p170])).
% 9.87/3.40  fof(sdef13, definition, (spl13 <=> (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 9.87/3.40  cnf(ssp11, plain, (spl1 | spl13), inference(avatar_split_clause, [status(thm)], [p480, sdef1, sdef13])).
% 9.87/3.40  cnf(p52, plain, ~apart_point_and_line(X0,line_connecting(sk1,X1)) | distinct_points(X0,sk1) | distinct_points(sk0,X2) | distinct_points(X2,X1), inference(resolution, [status(thm)], [c6, p22])).
% 9.87/3.40  cnf(p482, plain, distinct_points(X0,sk1) | distinct_points(sk0,X1) | distinct_points(X1,X2) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X2)) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p52, p205])).
% 9.87/3.40  fof(sdef14, definition, (spl14 <=> (distinct_points(sk0,X0) | distinct_points(X0,X1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X1)))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 9.87/3.40  cnf(ssp12, plain, (spl1 | spl14), inference(avatar_split_clause, [status(thm)], [p482, sdef1, sdef14])).
% 9.87/3.40  cnf(p61, plain, ~apart_point_and_line(X0,line_connecting(sk1,X1)) | distinct_points(X0,sk1) | distinct_points(sk2,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [c6, p24])).
% 9.87/3.40  cnf(p514, plain, distinct_points(X0,sk1) | distinct_points(sk2,X1) | distinct_points(X2,X1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X2)) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p61, p205])).
% 9.87/3.40  fof(sdef15, definition, (spl15 <=> (distinct_points(sk2,X0) | distinct_points(X1,X0) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X1)))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 9.87/3.40  cnf(ssp13, plain, (spl1 | spl15), inference(avatar_split_clause, [status(thm)], [p514, sdef1, sdef15])).
% 9.87/3.40  cnf(p122, plain, distinct_points(X0,sk1) | distinct_points(X0,X1) | distinct_points(sk2,X1), inference(resolution, [status(thm)], [p112, c3])).
% 9.87/3.40  cnf(p193, plain, distinct_points(X0,sk1) | distinct_points(sk2,X0), inference(resolution, [status(thm)], [p122, c0])).
% 9.87/3.40  cnf(p209, plain, distinct_points(sk2,X0) | ~apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(X1,sk1), inference(resolution, [status(thm)], [p193, c7])).
% 9.87/3.40  cnf(p517, plain, distinct_points(sk2,X0) | distinct_points(X1,sk1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk1)) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [p209, p205])).
% 9.87/3.40  fof(sdef16, definition, (spl16 <=> (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk1)))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 9.87/3.40  cnf(ssp14, plain, (spl1 | spl16), inference(avatar_split_clause, [status(thm)], [p517, sdef1, sdef16])).
% 9.87/3.40  cnf(p204, plain, distinct_lines(line_connecting(sk0,sk2),X0) | apart_point_and_line(sk1,X0), inference(resolution, [status(thm)], [c12, c18])).
% 9.87/3.40  fof(f4, axiom, ! [X,Y,Z] : ( distinct_lines(X,Y) => ( distinct_lines(X,Z) | distinct_lines(Y,Z) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', apart5)).
% 9.87/3.40  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])).
% 9.87/3.40  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])).
% 9.87/3.40  cnf(c4, plain, ~distinct_lines(X0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 9.87/3.40  cnf(p212, plain, apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p204, c4])).
% 9.87/3.40  cnf(p524, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk2),X0) | distinct_points(sk1,sk1), inference(resolution, [status(thm)], [p212, p47])).
% 9.87/3.40  fof(sdef17, definition, (spl17 <=> (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk2),X0))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 9.87/3.40  cnf(ssp15, plain, (spl8 | spl17), inference(avatar_split_clause, [status(thm)], [p524, sdef8, sdef17])).
% 9.87/3.40  cnf(p526, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk0),X0) | distinct_points(sk1,sk1), inference(resolution, [status(thm)], [p212, p70])).
% 9.87/3.40  fof(sdef18, definition, (spl18 <=> (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk0),X0))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 9.87/3.40  cnf(ssp16, plain, (spl8 | spl18), inference(avatar_split_clause, [status(thm)], [p526, sdef8, sdef18])).
% 9.87/3.40  cnf(p528, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk0,sk1),X0) | distinct_points(sk1,sk1), inference(resolution, [status(thm)], [p212, p71])).
% 9.87/3.40  fof(sdef19, definition, (spl19 <=> (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 9.87/3.40  cnf(ssp17, plain, (spl8 | spl19), inference(avatar_split_clause, [status(thm)], [p528, sdef8, sdef19])).
% 9.87/3.40  cnf(p530, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,sk1),X0) | distinct_points(sk1,sk1), inference(resolution, [status(thm)], [p212, p126])).
% 9.87/3.40  fof(sdef20, definition, (spl20 <=> (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,sk1),X0))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 9.87/3.40  cnf(ssp18, plain, (spl8 | spl20), inference(avatar_split_clause, [status(thm)], [p530, sdef8, sdef20])).
% 9.87/3.40  cnf(p533, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(sk1,sk1) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [p212, p48])).
% 9.87/3.40  fof(sdef21, definition, (spl21 <=> (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(sk0,X1))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 9.87/3.40  cnf(ssp19, plain, (spl8 | spl21), inference(avatar_split_clause, [status(thm)], [p533, sdef8, sdef21])).
% 9.87/3.40  cnf(p535, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(sk1,sk1) | distinct_points(X1,sk2), inference(resolution, [status(thm)], [p212, p64])).
% 9.87/3.40  fof(sdef22, definition, (spl22 <=> (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(X1,sk2))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 9.87/3.40  cnf(ssp20, plain, (spl8 | spl22), inference(avatar_split_clause, [status(thm)], [p535, sdef8, sdef22])).
% 9.87/3.40  cnf(p542, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(sk1,sk1) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [p212, p81])).
% 9.87/3.40  fof(sdef23, definition, (spl23 <=> (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(sk0,X1))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 9.87/3.40  cnf(ssp21, plain, (spl8 | spl23), inference(avatar_split_clause, [status(thm)], [p542, sdef8, sdef23])).
% 9.87/3.40  cnf(p544, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(sk1,sk1) | distinct_points(X1,sk0), inference(resolution, [status(thm)], [p212, p95])).
% 9.87/3.40  fof(sdef24, definition, (spl24 <=> (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(X1,sk0))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 9.87/3.40  cnf(ssp22, plain, (spl8 | spl24), inference(avatar_split_clause, [status(thm)], [p544, sdef8, sdef24])).
% 9.87/3.40  cnf(p548, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(X1,sk0) | distinct_points(sk1,sk1), inference(resolution, [status(thm)], [p212, p170])).
% 9.87/3.40  fof(sdef25, definition, (spl25 <=> (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(X1,sk0))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 9.87/3.40  cnf(ssp23, plain, (spl8 | spl25), inference(avatar_split_clause, [status(thm)], [p548, sdef8, sdef25])).
% 9.87/3.40  cnf(p550, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(sk1,sk1) | distinct_points(sk0,X2) | distinct_points(X2,X1), inference(resolution, [status(thm)], [p212, p52])).
% 9.87/3.40  fof(sdef26, definition, (spl26 <=> (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(sk0,X2) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 9.87/3.40  cnf(ssp24, plain, (spl8 | spl26), inference(avatar_split_clause, [status(thm)], [p550, sdef8, sdef26])).
% 9.87/3.40  cnf(p552, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(sk1,sk1) | distinct_points(sk2,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [p212, p61])).
% 9.87/3.40  fof(sdef27, definition, (spl27 <=> (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(sk2,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 9.87/3.40  cnf(ssp25, plain, (spl8 | spl27), inference(avatar_split_clause, [status(thm)], [p552, sdef8, sdef27])).
% 9.87/3.40  cnf(p554, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(sk2,X1) | distinct_points(sk1,sk1), inference(resolution, [status(thm)], [p212, p209])).
% 9.87/3.40  fof(sdef28, definition, (spl28 <=> (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(sk2,X1))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 9.87/3.40  cnf(ssp26, plain, (spl8 | spl28), inference(avatar_split_clause, [status(thm)], [p554, sdef8, sdef28])).
% 9.87/3.40  cnf(p63, plain, ~apart_point_and_line(X0,line_connecting(X1,X2)) | distinct_points(X0,X1) | distinct_points(sk1,X1) | distinct_points(sk2,X2), inference(resolution, [status(thm)], [c6, p24])).
% 9.87/3.40  cnf(p556, plain, ~apart_point_and_line(sk1,line_connecting(X0,X1)) | distinct_points(sk1,X0) | distinct_points(sk2,X1), inference(factoring, [status(thm)], [p63])).
% 9.87/3.40  cnf(p567, plain, distinct_points(sk1,X0) | distinct_points(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,X1)) | distinct_points(sk1,sk1), inference(resolution, [status(thm)], [p556, p205])).
% 9.87/3.40  fof(sdef29, definition, (spl29 <=> (distinct_points(sk1,X0) | distinct_points(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,X1)))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 9.87/3.40  cnf(ssp27, plain, (spl8 | spl29), inference(avatar_split_clause, [status(thm)], [p567, sdef8, sdef29])).
% 9.87/3.40  cnf(p77, plain, ~apart_point_and_line(X0,line_connecting(sk0,X1)) | distinct_points(X0,X1) | distinct_points(sk1,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [c7, p22])).
% 9.87/3.40  cnf(p635, plain, ~apart_point_and_line(sk1,line_connecting(sk0,X0)) | distinct_points(sk1,X0) | distinct_points(X0,X0), inference(factoring, [status(thm)], [p77])).
% 9.87/3.40  cnf(p639, plain, distinct_points(sk1,X0) | distinct_points(X0,X0) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk0,X0)) | distinct_points(sk1,sk1), inference(resolution, [status(thm)], [p635, p205])).
% 9.87/3.40  fof(sdef30, definition, (spl30 <=> (distinct_points(sk1,X0) | distinct_points(X0,X0) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk0,X0)))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 9.87/3.40  cnf(ssp28, plain, (spl8 | spl30), inference(avatar_split_clause, [status(thm)], [p639, sdef8, sdef30])).
% 9.87/3.40  cnf(p79, plain, ~apart_point_and_line(X0,line_connecting(X1,X2)) | distinct_points(X0,X2) | distinct_points(sk0,X1) | distinct_points(sk1,X2), inference(resolution, [status(thm)], [c7, p22])).
% 9.87/3.40  cnf(p702, plain, ~apart_point_and_line(sk1,line_connecting(X0,X1)) | distinct_points(sk1,X1) | distinct_points(sk0,X0), inference(factoring, [status(thm)], [p79])).
% 9.87/3.40  cnf(p711, plain, distinct_points(sk1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(X1,X0)) | distinct_points(sk1,sk1), inference(resolution, [status(thm)], [p702, p205])).
% 9.87/3.40  fof(sdef31, definition, (spl31 <=> (distinct_points(sk1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(X1,X0)))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 9.87/3.40  cnf(ssp29, plain, (spl8 | spl31), inference(avatar_split_clause, [status(thm)], [p711, sdef8, sdef31])).
% 9.87/3.40  cnf(p483, plain, (distinct_points(sk0,X0) | distinct_points(X0,X1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X1)) | ~spl14), inference(avatar_component_clause, [status(thm)], [sdef14])).
% 9.87/3.40  cnf(p870, plain, (distinct_points(sk0,sk0) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,sk0)) | ~spl14), inference(factoring, [status(thm)], [p483])).
% 9.87/3.40  cnf(ssp30, plain, (~spl14 | spl2 | spl32), inference(avatar_split_clause, [status(thm)], [p870, sdef2, sdef32])).
% 9.87/3.40  cnf(p92, plain, ~apart_point_and_line(X0,line_connecting(X1,sk1)) | distinct_points(X0,sk1) | distinct_points(sk0,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [c7, p29])).
% 9.87/3.40  cnf(p886, plain, distinct_points(X0,sk1) | distinct_points(sk0,X1) | distinct_points(X2,X1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(X2,sk1)) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p92, p205])).
% 9.87/3.40  fof(sdef33, definition, (spl33 <=> (distinct_points(sk0,X0) | distinct_points(X1,X0) | distinct_lines(line_connecting(sk0,sk2),line_connecting(X1,sk1)))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 9.87/3.40  cnf(ssp31, plain, (spl1 | spl33), inference(avatar_split_clause, [status(thm)], [p886, sdef1, sdef33])).
% 9.87/3.40  cnf(p888, plain, distinct_points(sk1,sk1) | distinct_points(sk0,X0) | distinct_points(X1,X0) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(line_connecting(X1,sk1),X2), inference(resolution, [status(thm)], [p92, p212])).
% 9.87/3.40  fof(sdef34, definition, (spl34 <=> (distinct_points(sk0,X0) | distinct_points(X1,X0) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(line_connecting(X1,sk1),X2))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 9.87/3.40  cnf(ssp32, plain, (spl8 | spl34), inference(avatar_split_clause, [status(thm)], [p888, sdef8, sdef34])).
% 9.87/3.40  cnf(p93, plain, ~apart_point_and_line(X0,line_connecting(sk0,X1)) | distinct_points(X0,X1) | distinct_points(X2,sk1) | distinct_points(X2,X1), inference(resolution, [status(thm)], [c7, p29])).
% 9.87/3.40  cnf(p897, plain, ~apart_point_and_line(X0,line_connecting(sk0,X1)) | distinct_points(X0,X1) | distinct_points(X0,sk1), inference(factoring, [status(thm)], [p93])).
% 9.87/3.40  cnf(p901, plain, distinct_points(sk1,X0) | distinct_points(sk1,sk1) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(line_connecting(sk0,X0),X1), inference(resolution, [status(thm)], [p897, p212])).
% 9.87/3.40  fof(sdef35, definition, (spl35 <=> (distinct_points(sk1,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(line_connecting(sk0,X0),X1))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 9.87/3.40  cnf(ssp33, plain, (spl8 | spl35), inference(avatar_split_clause, [status(thm)], [p901, sdef8, sdef35])).
% 9.87/3.40  cnf(p515, plain, (distinct_points(sk2,X0) | distinct_points(X1,X0) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X1)) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 9.87/3.40  cnf(p925, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,sk2)) | ~spl15), inference(factoring, [status(thm)], [p515])).
% 9.87/3.40  cnf(ssp34, plain, (~spl15 | spl0 | spl36), inference(avatar_split_clause, [status(thm)], [p925, sdef0, sdef36])).
% 9.87/3.40  cnf(p116, plain, distinct_points(X0,sk2) | distinct_points(X0,X1) | ~apart_point_and_line(X2,line_connecting(sk1,X1)) | distinct_points(X2,sk1), inference(resolution, [status(thm)], [p39, c6])).
% 9.87/3.40  cnf(p969, plain, distinct_points(X0,sk2) | distinct_points(X0,X1) | distinct_points(X2,sk1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X1)) | distinct_points(sk1,X2), inference(resolution, [status(thm)], [p116, p205])).
% 9.87/3.40  fof(sdef37, definition, (spl37 <=> (distinct_points(X0,sk2) | distinct_points(X0,X1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X1)))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 9.87/3.40  cnf(ssp35, plain, (spl1 | spl37), inference(avatar_split_clause, [status(thm)], [p969, sdef1, sdef37])).
% 9.87/3.40  cnf(p971, plain, distinct_points(X0,sk2) | distinct_points(X0,X1) | distinct_points(sk1,sk1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(line_connecting(sk1,X1),X2), inference(resolution, [status(thm)], [p116, p212])).
% 9.87/3.40  fof(sdef38, definition, (spl38 <=> (distinct_points(X0,sk2) | distinct_points(X0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(line_connecting(sk1,X1),X2))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 9.87/3.40  cnf(ssp36, plain, (spl8 | spl38), inference(avatar_split_clause, [status(thm)], [p971, sdef8, sdef38])).
% 9.87/3.40  cnf(p120, plain, distinct_points(X0,sk2) | distinct_points(sk1,X1) | ~apart_point_and_line(X2,line_connecting(X0,X1)) | distinct_points(X2,X1), inference(resolution, [status(thm)], [p39, c7])).
% 9.87/3.40  cnf(p1000, plain, distinct_points(X0,sk2) | distinct_points(sk1,X1) | ~apart_point_and_line(sk1,line_connecting(X0,X1)), inference(factoring, [status(thm)], [p120])).
% 9.87/3.40  cnf(p1003, plain, distinct_points(X0,sk2) | distinct_points(sk1,X1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,X1)) | distinct_points(sk1,sk1), inference(resolution, [status(thm)], [p1000, p205])).
% 9.87/3.40  fof(sdef39, definition, (spl39 <=> (distinct_points(X0,sk2) | distinct_points(sk1,X1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,X1)))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 9.87/3.40  cnf(ssp37, plain, (spl8 | spl39), inference(avatar_split_clause, [status(thm)], [p1003, sdef8, sdef39])).
% 9.87/3.40  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/sandbox/benchmark/theBenchmark.p', cu1)).
% 9.87/3.40  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])).
% 9.87/3.40  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])).
% 9.87/3.40  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])).
% 9.87/3.40  cnf(p127, 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])).
% 9.87/3.40  cnf(p451, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,sk2)) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 9.87/3.40  cnf(p485, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk2),X0) | ~spl0), inference(resolution, [status(thm)], [p451, c4])).
% 9.87/3.40  cnf(p508, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk2),X1) | distinct_lines(X0,X1) | ~spl0), inference(resolution, [status(thm)], [p485, c4])).
% 9.87/3.40  cnf(p1030, 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,sk2),X1) | distinct_lines(X1,X0) | ~spl0), inference(resolution, [status(thm)], [p127, p508])).
% 9.87/3.40  fof(sdef40, definition, (spl40 <=> (apart_point_and_line(sk0,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 9.87/3.40  fof(sdef41, definition, (spl41 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 9.87/3.40  cnf(ssp38, plain, (~spl0 | spl40 | spl41 | spl42), inference(avatar_split_clause, [status(thm)], [p1030, sdef40, sdef41, sdef42])).
% 9.87/3.40  cnf(p454, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,sk0)) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 9.87/3.40  cnf(p497, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk0),X0) | ~spl2), inference(resolution, [status(thm)], [p454, c4])).
% 9.87/3.40  cnf(p510, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk0),X1) | distinct_lines(X0,X1) | ~spl2), inference(resolution, [status(thm)], [p497, c4])).
% 9.87/3.40  cnf(p1034, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl2), inference(resolution, [status(thm)], [p127, p510])).
% 9.87/3.40  cnf(ssp39, plain, (~spl2 | spl41 | spl43 | spl44), inference(avatar_split_clause, [status(thm)], [p1034, sdef41, sdef43, sdef44])).
% 9.87/3.40  cnf(p458, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk2,sk1)) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 9.87/3.40  cnf(p499, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,sk1),X0) | ~spl4), inference(resolution, [status(thm)], [p458, c4])).
% 9.87/3.40  cnf(p513, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl4), inference(resolution, [status(thm)], [p499, c4])).
% 9.87/3.40  cnf(p1037, 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,sk2),X1) | distinct_lines(X1,X0) | ~spl4), inference(resolution, [status(thm)], [p127, p513])).
% 9.87/3.41  fof(sdef45, definition, (spl45 <=> (apart_point_and_line(sk0,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 9.87/3.41  cnf(ssp40, plain, (~spl4 | spl41 | spl45 | spl46), inference(avatar_split_clause, [status(thm)], [p1037, sdef41, sdef45, sdef46])).
% 9.87/3.41  cnf(p525, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk2),X0) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 9.87/3.41  cnf(p560, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk2),X1) | distinct_lines(X0,X1) | ~spl17), inference(resolution, [status(thm)], [p525, c4])).
% 9.87/3.41  cnf(p1040, 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,sk2),X1) | distinct_lines(X1,X0) | ~spl17), inference(resolution, [status(thm)], [p127, p560])).
% 9.87/3.41  cnf(ssp41, plain, (~spl17 | spl40 | spl41 | spl42), inference(avatar_split_clause, [status(thm)], [p1040, sdef40, sdef41, sdef42])).
% 9.87/3.41  cnf(p527, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk0),X0) | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 9.87/3.41  cnf(p562, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk0),X1) | distinct_lines(X0,X1) | ~spl18), inference(resolution, [status(thm)], [p527, c4])).
% 9.87/3.41  cnf(p1041, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl18), inference(resolution, [status(thm)], [p127, p562])).
% 9.87/3.41  cnf(ssp42, plain, (~spl18 | spl41 | spl43 | spl44), inference(avatar_split_clause, [status(thm)], [p1041, sdef41, sdef43, sdef44])).
% 9.87/3.41  cnf(p531, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,sk1),X0) | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 9.87/3.41  cnf(p566, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl20), inference(resolution, [status(thm)], [p531, c4])).
% 9.87/3.41  cnf(p1042, 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,sk2),X1) | distinct_lines(X1,X0) | ~spl20), inference(resolution, [status(thm)], [p127, p566])).
% 9.87/3.41  cnf(ssp43, plain, (~spl20 | spl41 | spl45 | spl46), inference(avatar_split_clause, [status(thm)], [p1042, sdef41, sdef45, sdef46])).
% 9.87/3.41  cnf(p128, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1), inference(resolution, [status(thm)], [c10, c15])).
% 9.87/3.41  cnf(p1052, plain, apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk1,X0), inference(resolution, [status(thm)], [p128, p204])).
% 9.87/3.41  fof(sdef48, definition, (spl48 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk1,X0))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 9.87/3.41  cnf(ssp44, plain, (spl47 | spl48 | spl49), inference(avatar_split_clause, [status(thm)], [p1052, sdef47, sdef48, sdef49])).
% 9.87/3.41  cnf(p1056, plain, apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,X0) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [p128, p205])).
% 9.87/3.41  fof(sdef50, definition, (spl50 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,X0) | distinct_points(sk1,X1))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 9.87/3.41  cnf(ssp45, plain, (spl47 | spl49 | spl50), inference(avatar_split_clause, [status(thm)], [p1056, sdef47, sdef49, sdef50])).
% 9.87/3.41  cnf(p1058, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,sk2)) | ~spl0), inference(resolution, [status(thm)], [p128, p451])).
% 9.87/3.41  cnf(ssp46, plain, (~spl0 | spl40 | spl47 | spl49 | spl51), inference(avatar_split_clause, [status(thm)], [p1058, sdef40, sdef47, sdef49, sdef51])).
% 9.87/3.41  cnf(p1060, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | ~spl2), inference(resolution, [status(thm)], [p128, p454])).
% 9.87/3.41  fof(sdef52, definition, (spl52 <=> (apart_point_and_line(sk2,line_connecting(sk1,sk0)))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 9.87/3.41  cnf(ssp47, plain, (~spl2 | spl43 | spl47 | spl49 | spl52), inference(avatar_split_clause, [status(thm)], [p1060, sdef43, sdef47, sdef49, sdef52])).
% 9.87/3.41  cnf(p456, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk0,sk1)) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 9.87/3.41  cnf(p1062, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | ~spl3), inference(resolution, [status(thm)], [p128, p456])).
% 9.87/3.41  cnf(ssp48, plain, (~spl3 | spl47 | spl49 | spl53 | spl54), inference(avatar_split_clause, [status(thm)], [p1062, sdef47, sdef49, sdef53, sdef54])).
% 9.87/3.41  cnf(p1065, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | ~spl4), inference(resolution, [status(thm)], [p128, p458])).
% 9.87/3.41  fof(sdef55, definition, (spl55 <=> (apart_point_and_line(sk2,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 9.87/3.41  cnf(ssp49, plain, (~spl4 | spl45 | spl47 | spl49 | spl55), inference(avatar_split_clause, [status(thm)], [p1065, sdef45, sdef47, sdef49, sdef55])).
% 9.87/3.41  cnf(p461, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | distinct_points(sk0,X0) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 9.87/3.41  cnf(p1067, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(sk0,X0) | ~spl5), inference(resolution, [status(thm)], [p128, p461])).
% 9.87/3.41  fof(sdef56, definition, (spl56 <=> (apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 9.87/3.41  cnf(ssp50, plain, (~spl5 | spl47 | spl49 | spl56), inference(avatar_split_clause, [status(thm)], [p1067, sdef47, sdef49, sdef56])).
% 9.87/3.41  cnf(p463, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | distinct_points(X0,sk2) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 9.87/3.41  cnf(p1069, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(X0,sk2) | ~spl6), inference(resolution, [status(thm)], [p128, p463])).
% 9.87/3.41  fof(sdef57, definition, (spl57 <=> (apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(X0,sk2))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 9.87/3.41  cnf(ssp51, plain, (~spl6 | spl47 | spl49 | spl57), inference(avatar_split_clause, [status(thm)], [p1069, sdef47, sdef49, sdef57])).
% 9.87/3.41  cnf(p473, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk1)) | distinct_points(sk0,X0) | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 9.87/3.41  cnf(p1071, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | distinct_points(sk0,X0) | ~spl10), inference(resolution, [status(thm)], [p128, p473])).
% 9.87/3.41  fof(sdef58, definition, (spl58 <=> (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 9.87/3.41  cnf(ssp52, plain, (~spl10 | spl47 | spl49 | spl58), inference(avatar_split_clause, [status(thm)], [p1071, sdef47, sdef49, sdef58])).
% 9.87/3.41  cnf(p475, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk1)) | distinct_points(X0,sk0) | ~spl11), inference(avatar_component_clause, [status(thm)], [sdef11])).
% 9.87/3.41  cnf(p1073, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | distinct_points(X0,sk0) | ~spl11), inference(resolution, [status(thm)], [p128, p475])).
% 9.87/3.41  fof(sdef59, definition, (spl59 <=> (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 9.87/3.41  cnf(ssp53, plain, (~spl11 | spl47 | spl49 | spl59), inference(avatar_split_clause, [status(thm)], [p1073, sdef47, sdef49, sdef59])).
% 9.87/3.41  cnf(p481, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | distinct_points(X0,sk0) | ~spl13), inference(avatar_component_clause, [status(thm)], [sdef13])).
% 9.87/3.41  cnf(p1075, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(X0,sk0) | ~spl13), inference(resolution, [status(thm)], [p128, p481])).
% 9.87/3.41  fof(sdef60, definition, (spl60 <=> (apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 9.87/3.41  cnf(ssp54, plain, (~spl13 | spl47 | spl49 | spl60), inference(avatar_split_clause, [status(thm)], [p1075, sdef47, sdef49, sdef60])).
% 9.87/3.41  cnf(p1077, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl0), inference(resolution, [status(thm)], [p128, p485])).
% 9.87/3.41  fof(sdef61, definition, (spl61 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X0))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 9.87/3.41  cnf(ssp55, plain, (~spl0 | spl40 | spl51 | spl61), inference(avatar_split_clause, [status(thm)], [p1077, sdef40, sdef51, sdef61])).
% 9.87/3.41  cnf(p1079, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl2), inference(resolution, [status(thm)], [p128, p497])).
% 9.87/3.41  cnf(ssp56, plain, (~spl2 | spl43 | spl52 | spl61), inference(avatar_split_clause, [status(thm)], [p1079, sdef43, sdef52, sdef61])).
% 9.87/3.41  cnf(p498, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl3), inference(resolution, [status(thm)], [p456, c4])).
% 9.87/3.41  cnf(p1080, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl3), inference(resolution, [status(thm)], [p128, p498])).
% 9.87/3.41  fof(sdef62, definition, (spl62 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 9.87/3.41  cnf(ssp57, plain, (~spl3 | spl47 | spl49 | spl62), inference(avatar_split_clause, [status(thm)], [p1080, sdef47, sdef49, sdef62])).
% 9.87/3.41  cnf(p1082, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl4), inference(resolution, [status(thm)], [p128, p499])).
% 9.87/3.41  cnf(ssp58, plain, (~spl4 | spl45 | spl55 | spl61), inference(avatar_split_clause, [status(thm)], [p1082, sdef45, sdef55, sdef61])).
% 9.87/3.41  cnf(p518, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,sk1)) | ~spl16), inference(avatar_component_clause, [status(thm)], [sdef16])).
% 9.87/3.41  cnf(p1083, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | distinct_points(sk2,X0) | ~spl16), inference(resolution, [status(thm)], [p128, p518])).
% 9.87/3.41  fof(sdef63, definition, (spl63 <=> (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 9.87/3.41  cnf(ssp59, plain, (~spl16 | spl47 | spl49 | spl63), inference(avatar_split_clause, [status(thm)], [p1083, sdef47, sdef49, sdef63])).
% 9.87/3.41  cnf(p1085, plain, apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p128, p212])).
% 9.87/3.41  fof(sdef64, definition, (spl64 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 9.87/3.41  cnf(ssp60, plain, (spl47 | spl49 | spl64), inference(avatar_split_clause, [status(thm)], [p1085, sdef47, sdef49, sdef64])).
% 9.87/3.41  cnf(p1087, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk2),X1), inference(resolution, [status(thm)], [p128, p212])).
% 9.87/3.41  cnf(ssp61, plain, (spl48 | spl61), inference(avatar_split_clause, [status(thm)], [p1087, sdef48, sdef61])).
% 9.87/3.41  cnf(p1088, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl17), inference(resolution, [status(thm)], [p128, p525])).
% 9.87/3.41  cnf(ssp62, plain, (~spl17 | spl40 | spl51 | spl61), inference(avatar_split_clause, [status(thm)], [p1088, sdef40, sdef51, sdef61])).
% 9.87/3.41  fof(f1, axiom, ! [X] : ~ distinct_lines(X,X), file('/export/starexec/sandbox/benchmark/theBenchmark.p', apart2)).
% 9.87/3.41  fof(f1_nnf, plain, ! [X] : (~(distinct_lines(X,X))), inference(nnf_transformation, [status(thm)], [f1])).
% 9.87/3.41  fof(f1_sk, plain, ! [X] : (~(distinct_lines(X,X))), inference(skolemisation, [status(esa)], [f1_nnf])).
% 9.87/3.41  cnf(c1, plain, ~distinct_lines(X0,X0), inference(cnf_transformation, [status(esa)], [f1_sk])).
% 9.87/3.41  cnf(p559, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,sk2)) | ~spl17), inference(resolution, [status(thm)], [p525, c1])).
% 9.87/3.41  cnf(p1089, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,sk2)) | ~spl17), inference(resolution, [status(thm)], [p128, p559])).
% 9.87/3.41  cnf(ssp63, plain, (~spl17 | spl40 | spl47 | spl49 | spl51), inference(avatar_split_clause, [status(thm)], [p1089, sdef40, sdef47, sdef49, sdef51])).
% 9.87/3.41  cnf(p1090, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl18), inference(resolution, [status(thm)], [p128, p527])).
% 9.87/3.41  cnf(ssp64, plain, (~spl18 | spl43 | spl52 | spl61), inference(avatar_split_clause, [status(thm)], [p1090, sdef43, sdef52, sdef61])).
% 9.87/3.41  cnf(p561, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,sk0)) | ~spl18), inference(resolution, [status(thm)], [p527, c1])).
% 9.87/3.41  cnf(p1091, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | ~spl18), inference(resolution, [status(thm)], [p128, p561])).
% 9.87/3.41  cnf(ssp65, plain, (~spl18 | spl43 | spl47 | spl49 | spl52), inference(avatar_split_clause, [status(thm)], [p1091, sdef43, sdef47, sdef49, sdef52])).
% 9.87/3.41  cnf(p529, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 9.87/3.41  cnf(p1092, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl19), inference(resolution, [status(thm)], [p128, p529])).
% 9.87/3.41  cnf(ssp66, plain, (~spl19 | spl47 | spl49 | spl62), inference(avatar_split_clause, [status(thm)], [p1092, sdef47, sdef49, sdef62])).
% 9.87/3.41  cnf(p563, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)) | ~spl19), inference(resolution, [status(thm)], [p529, c1])).
% 9.87/3.41  cnf(p1093, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | ~spl19), inference(resolution, [status(thm)], [p128, p563])).
% 9.87/3.41  cnf(ssp67, plain, (~spl19 | spl47 | spl49 | spl53 | spl54), inference(avatar_split_clause, [status(thm)], [p1093, sdef47, sdef49, sdef53, sdef54])).
% 9.87/3.41  cnf(p1094, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl20), inference(resolution, [status(thm)], [p128, p531])).
% 9.87/3.41  cnf(ssp68, plain, (~spl20 | spl45 | spl55 | spl61), inference(avatar_split_clause, [status(thm)], [p1094, sdef45, sdef55, sdef61])).
% 9.87/3.41  cnf(p565, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk2,sk1)) | ~spl20), inference(resolution, [status(thm)], [p531, c1])).
% 9.87/3.41  cnf(p1095, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | ~spl20), inference(resolution, [status(thm)], [p128, p565])).
% 9.87/3.41  cnf(ssp69, plain, (~spl20 | spl45 | spl47 | spl49 | spl55), inference(avatar_split_clause, [status(thm)], [p1095, sdef45, sdef47, sdef49, sdef55])).
% 9.87/3.41  cnf(p1096, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(X1,X0) | ~spl14), inference(resolution, [status(thm)], [p128, p483])).
% 9.87/3.41  fof(sdef65, definition, (spl65 <=> (apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(X1,X0))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 9.87/3.41  cnf(ssp70, plain, (~spl14 | spl47 | spl49 | spl65), inference(avatar_split_clause, [status(thm)], [p1096, sdef47, sdef49, sdef65])).
% 9.87/3.41  cnf(p872, plain, (distinct_points(sk0,X0) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | ~spl14), inference(resolution, [status(thm)], [p483, c0])).
% 9.87/3.41  cnf(p1098, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(sk0,X0) | ~spl14), inference(resolution, [status(thm)], [p128, p872])).
% 9.87/3.41  cnf(ssp71, plain, (~spl14 | spl47 | spl49 | spl56), inference(avatar_split_clause, [status(thm)], [p1098, sdef47, sdef49, sdef56])).
% 9.87/3.41  cnf(p500, plain, (distinct_points(sk0,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(line_connecting(sk1,X0),X1) | ~spl5), inference(resolution, [status(thm)], [p461, c4])).
% 9.87/3.41  cnf(p1099, plain, (apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(sk2,X1) | distinct_points(sk0,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | ~spl5), inference(resolution, [status(thm)], [p128, p500])).
% 9.87/3.41  cnf(ssp72, plain, (~spl5 | spl56 | spl61), inference(avatar_split_clause, [status(thm)], [p1099, sdef56, sdef61])).
% 9.87/3.41  cnf(p501, plain, (distinct_points(X0,sk2) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(line_connecting(sk1,X0),X1) | ~spl6), inference(resolution, [status(thm)], [p463, c4])).
% 9.87/3.41  cnf(p1100, plain, (apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(sk2,X1) | distinct_points(X0,sk2) | distinct_lines(line_connecting(sk0,sk2),X1) | ~spl6), inference(resolution, [status(thm)], [p128, p501])).
% 9.87/3.41  cnf(ssp73, plain, (~spl6 | spl57 | spl61), inference(avatar_split_clause, [status(thm)], [p1100, sdef57, sdef61])).
% 9.87/3.41  cnf(p504, plain, (distinct_points(sk0,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(line_connecting(X0,sk1),X1) | ~spl10), inference(resolution, [status(thm)], [p473, c4])).
% 9.87/3.41  cnf(p1101, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(X1,sk1),X0) | ~spl10), inference(resolution, [status(thm)], [p128, p504])).
% 9.87/3.41  fof(sdef66, definition, (spl66 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(X1,sk1),X0))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 9.87/3.41  cnf(ssp74, plain, (~spl10 | spl47 | spl49 | spl66), inference(avatar_split_clause, [status(thm)], [p1101, sdef47, sdef49, sdef66])).
% 9.87/3.41  cnf(p1103, plain, (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,X1) | distinct_points(sk0,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | ~spl10), inference(resolution, [status(thm)], [p128, p504])).
% 9.87/3.41  cnf(ssp75, plain, (~spl10 | spl58 | spl61), inference(avatar_split_clause, [status(thm)], [p1103, sdef58, sdef61])).
% 9.87/3.41  cnf(p505, plain, (distinct_points(X0,sk0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(line_connecting(X0,sk1),X1) | ~spl11), inference(resolution, [status(thm)], [p475, c4])).
% 9.87/3.41  cnf(p1104, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_points(X1,sk0) | distinct_lines(line_connecting(X1,sk1),X0) | ~spl11), inference(resolution, [status(thm)], [p128, p505])).
% 9.87/3.41  fof(sdef67, definition, (spl67 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_points(X1,sk0) | distinct_lines(line_connecting(X1,sk1),X0))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 9.87/3.41  cnf(ssp76, plain, (~spl11 | spl47 | spl49 | spl67), inference(avatar_split_clause, [status(thm)], [p1104, sdef47, sdef49, sdef67])).
% 9.87/3.41  cnf(p1106, plain, (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,X1) | distinct_points(X0,sk0) | distinct_lines(line_connecting(sk0,sk2),X1) | ~spl11), inference(resolution, [status(thm)], [p128, p505])).
% 9.87/3.41  cnf(ssp77, plain, (~spl11 | spl59 | spl61), inference(avatar_split_clause, [status(thm)], [p1106, sdef59, sdef61])).
% 9.87/3.41  cnf(p507, plain, (distinct_points(X0,sk0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(line_connecting(sk1,X0),X1) | ~spl13), inference(resolution, [status(thm)], [p481, c4])).
% 9.87/3.41  cnf(p1107, plain, (apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(sk2,X1) | distinct_points(X0,sk0) | distinct_lines(line_connecting(sk0,sk2),X1) | ~spl13), inference(resolution, [status(thm)], [p128, p507])).
% 9.87/3.41  cnf(ssp78, plain, (~spl13 | spl60 | spl61), inference(avatar_split_clause, [status(thm)], [p1107, sdef60, sdef61])).
% 9.87/3.41  cnf(p1108, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk2),X1) | distinct_lines(X0,X1) | ~spl0), inference(resolution, [status(thm)], [p128, p508])).
% 9.87/3.41  fof(sdef68, definition, (spl68 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk2),X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 9.87/3.41  cnf(ssp79, plain, (~spl0 | spl47 | spl49 | spl68), inference(avatar_split_clause, [status(thm)], [p1108, sdef47, sdef49, sdef68])).
% 9.87/3.41  cnf(p1110, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl0), inference(resolution, [status(thm)], [p128, p508])).
% 9.87/3.41  fof(sdef69, definition, (spl69 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 9.87/3.41  cnf(ssp80, plain, (~spl0 | spl40 | spl51 | spl69), inference(avatar_split_clause, [status(thm)], [p1110, sdef40, sdef51, sdef69])).
% 9.87/3.41  cnf(p1112, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk2),X1) | ~spl0), inference(resolution, [status(thm)], [p128, p508])).
% 9.87/3.41  fof(sdef70, definition, (spl70 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk2),X0))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 9.87/3.41  cnf(ssp81, plain, (~spl0 | spl61 | spl70), inference(avatar_split_clause, [status(thm)], [p1112, sdef61, sdef70])).
% 9.87/3.41  cnf(p904, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(X0,line_connecting(sk1,sk2)) | ~spl0), inference(resolution, [status(thm)], [p508, c1])).
% 9.87/3.41  cnf(p1114, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk1,sk2)) | ~spl0), inference(resolution, [status(thm)], [p128, p904])).
% 9.87/3.41  fof(sdef71, definition, (spl71 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 9.87/3.41  cnf(ssp82, plain, (~spl0 | spl47 | spl49 | spl71), inference(avatar_split_clause, [status(thm)], [p1114, sdef47, sdef49, sdef71])).
% 9.87/3.41  cnf(p1116, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk0),X1) | distinct_lines(X0,X1) | ~spl2), inference(resolution, [status(thm)], [p128, p510])).
% 9.87/3.41  fof(sdef72, definition, (spl72 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk0),X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 9.87/3.41  cnf(ssp83, plain, (~spl2 | spl47 | spl49 | spl72), inference(avatar_split_clause, [status(thm)], [p1116, sdef47, sdef49, sdef72])).
% 9.87/3.41  cnf(p1118, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl2), inference(resolution, [status(thm)], [p128, p510])).
% 9.87/3.41  cnf(ssp84, plain, (~spl2 | spl43 | spl52 | spl69), inference(avatar_split_clause, [status(thm)], [p1118, sdef43, sdef52, sdef69])).
% 9.87/3.41  cnf(p1119, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk0),X1) | ~spl2), inference(resolution, [status(thm)], [p128, p510])).
% 9.87/3.41  fof(sdef73, definition, (spl73 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk0),X0))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 9.87/3.41  cnf(ssp85, plain, (~spl2 | spl61 | spl73), inference(avatar_split_clause, [status(thm)], [p1119, sdef61, sdef73])).
% 9.87/3.41  cnf(p910, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(X0,line_connecting(sk1,sk0)) | ~spl2), inference(resolution, [status(thm)], [p510, c1])).
% 9.87/3.41  cnf(p1121, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk1,sk0)) | ~spl2), inference(resolution, [status(thm)], [p128, p910])).
% 9.87/3.41  fof(sdef74, definition, (spl74 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk1,sk0)))), introduced(definition, [new_symbols(naming, [spl74])], [avatar_definition])).
% 9.87/3.41  cnf(ssp86, plain, (~spl2 | spl47 | spl49 | spl74), inference(avatar_split_clause, [status(thm)], [p1121, sdef47, sdef49, sdef74])).
% 9.87/3.41  cnf(p512, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X0,X1) | ~spl3), inference(resolution, [status(thm)], [p498, c4])).
% 9.87/3.41  cnf(p1123, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X0,X1) | ~spl3), inference(resolution, [status(thm)], [p128, p512])).
% 9.87/3.41  fof(sdef75, definition, (spl75 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl75])], [avatar_definition])).
% 9.87/3.41  cnf(ssp87, plain, (~spl3 | spl53 | spl54 | spl75), inference(avatar_split_clause, [status(thm)], [p1123, sdef53, sdef54, sdef75])).
% 9.87/3.41  cnf(p1125, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X1,X0) | ~spl3), inference(resolution, [status(thm)], [p128, p512])).
% 9.87/3.41  fof(sdef76, definition, (spl76 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl76])], [avatar_definition])).
% 9.87/3.41  cnf(ssp88, plain, (~spl3 | spl47 | spl49 | spl76), inference(avatar_split_clause, [status(thm)], [p1125, sdef47, sdef49, sdef76])).
% 9.87/3.41  cnf(p1127, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X1) | ~spl3), inference(resolution, [status(thm)], [p128, p512])).
% 9.87/3.41  cnf(ssp89, plain, (~spl3 | spl61 | spl62), inference(avatar_split_clause, [status(thm)], [p1127, sdef61, sdef62])).
% 9.87/3.41  cnf(p915, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(X0,line_connecting(sk0,sk2)) | ~spl3), inference(resolution, [status(thm)], [p512, c1])).
% 9.87/3.41  cnf(p1128, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk0,sk2)) | ~spl3), inference(resolution, [status(thm)], [p128, p915])).
% 9.87/3.41  fof(sdef77, definition, (spl77 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl77])], [avatar_definition])).
% 9.87/3.41  cnf(ssp90, plain, (~spl3 | spl53 | spl54 | spl77), inference(avatar_split_clause, [status(thm)], [p1128, sdef53, sdef54, sdef77])).
% 9.87/3.41  cnf(p1130, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl4), inference(resolution, [status(thm)], [p128, p513])).
% 9.87/3.41  fof(sdef78, definition, (spl78 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl78])], [avatar_definition])).
% 9.87/3.41  cnf(ssp91, plain, (~spl4 | spl47 | spl49 | spl78), inference(avatar_split_clause, [status(thm)], [p1130, sdef47, sdef49, sdef78])).
% 9.87/3.41  cnf(p1132, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl4), inference(resolution, [status(thm)], [p128, p513])).
% 9.87/3.41  cnf(ssp92, plain, (~spl4 | spl45 | spl55 | spl69), inference(avatar_split_clause, [status(thm)], [p1132, sdef45, sdef55, sdef69])).
% 9.87/3.41  cnf(p1133, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl4), inference(resolution, [status(thm)], [p128, p513])).
% 9.87/3.41  fof(sdef79, definition, (spl79 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X0))), introduced(definition, [new_symbols(naming, [spl79])], [avatar_definition])).
% 9.87/3.41  cnf(ssp93, plain, (~spl4 | spl61 | spl79), inference(avatar_split_clause, [status(thm)], [p1133, sdef61, sdef79])).
% 9.87/3.41  cnf(p920, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl4), inference(resolution, [status(thm)], [p513, c1])).
% 9.87/3.41  cnf(p1135, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl4), inference(resolution, [status(thm)], [p128, p920])).
% 9.87/3.41  fof(sdef80, definition, (spl80 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl80])], [avatar_definition])).
% 9.87/3.41  cnf(ssp94, plain, (~spl4 | spl47 | spl49 | spl80), inference(avatar_split_clause, [status(thm)], [p1135, sdef47, sdef49, sdef80])).
% 9.87/3.41  cnf(p1137, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(sk2,X1) | distinct_points(X0,X1) | ~spl15), inference(resolution, [status(thm)], [p128, p515])).
% 9.87/3.41  fof(sdef81, definition, (spl81 <=> (apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(sk2,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl81])], [avatar_definition])).
% 9.87/3.41  cnf(ssp95, plain, (~spl15 | spl47 | spl49 | spl81), inference(avatar_split_clause, [status(thm)], [p1137, sdef47, sdef49, sdef81])).
% 9.87/3.41  cnf(p927, plain, (distinct_points(X0,sk2) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | ~spl15), inference(resolution, [status(thm)], [p515, c0])).
% 9.87/3.41  cnf(p1139, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(X0,sk2) | ~spl15), inference(resolution, [status(thm)], [p128, p927])).
% 9.87/3.41  cnf(ssp96, plain, (~spl15 | spl47 | spl49 | spl57), inference(avatar_split_clause, [status(thm)], [p1139, sdef47, sdef49, sdef57])).
% 9.87/3.41  cnf(p928, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | ~spl15), inference(resolution, [status(thm)], [p515, c0])).
% 9.87/3.41  cnf(p1140, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(sk2,X0) | ~spl15), inference(resolution, [status(thm)], [p128, p928])).
% 9.87/3.41  fof(sdef82, definition, (spl82 <=> (apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl82])], [avatar_definition])).
% 9.87/3.41  cnf(ssp97, plain, (~spl15 | spl47 | spl49 | spl82), inference(avatar_split_clause, [status(thm)], [p1140, sdef47, sdef49, sdef82])).
% 9.87/3.41  cnf(p519, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(line_connecting(X0,sk1),X1) | ~spl16), inference(resolution, [status(thm)], [p518, c4])).
% 9.87/3.41  cnf(p1142, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_points(sk2,X1) | distinct_lines(line_connecting(X1,sk1),X0) | ~spl16), inference(resolution, [status(thm)], [p128, p519])).
% 9.87/3.41  fof(sdef83, definition, (spl83 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_points(sk2,X1) | distinct_lines(line_connecting(X1,sk1),X0))), introduced(definition, [new_symbols(naming, [spl83])], [avatar_definition])).
% 9.87/3.41  cnf(ssp98, plain, (~spl16 | spl47 | spl49 | spl83), inference(avatar_split_clause, [status(thm)], [p1142, sdef47, sdef49, sdef83])).
% 9.87/3.41  cnf(p1144, plain, (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,X1) | distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | ~spl16), inference(resolution, [status(thm)], [p128, p519])).
% 9.87/3.41  cnf(ssp99, plain, (~spl16 | spl61 | spl63), inference(avatar_split_clause, [status(thm)], [p1144, sdef61, sdef63])).
% 9.87/3.41  cnf(p534, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(sk0,X1) | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 9.87/3.41  cnf(p1145, plain, (apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_points(sk0,X0) | ~spl21), inference(resolution, [status(thm)], [p128, p534])).
% 9.87/3.41  cnf(ssp100, plain, (~spl21 | spl56 | spl61), inference(avatar_split_clause, [status(thm)], [p1145, sdef56, sdef61])).
% 9.87/3.41  cnf(p944, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | distinct_points(sk0,X0) | ~spl21), inference(resolution, [status(thm)], [p534, c1])).
% 9.87/3.41  cnf(p1146, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(sk0,X0) | ~spl21), inference(resolution, [status(thm)], [p128, p944])).
% 9.87/3.41  cnf(ssp101, plain, (~spl21 | spl47 | spl49 | spl56), inference(avatar_split_clause, [status(thm)], [p1146, sdef47, sdef49, sdef56])).
% 9.87/3.41  cnf(p536, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(X1,sk2) | ~spl22), inference(avatar_component_clause, [status(thm)], [sdef22])).
% 9.87/3.41  cnf(p1147, plain, (apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_points(X0,sk2) | ~spl22), inference(resolution, [status(thm)], [p128, p536])).
% 9.87/3.41  cnf(ssp102, plain, (~spl22 | spl57 | spl61), inference(avatar_split_clause, [status(thm)], [p1147, sdef57, sdef61])).
% 9.87/3.41  cnf(p946, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | distinct_points(X0,sk2) | ~spl22), inference(resolution, [status(thm)], [p536, c1])).
% 9.87/3.41  cnf(p1148, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(X0,sk2) | ~spl22), inference(resolution, [status(thm)], [p128, p946])).
% 9.87/3.41  cnf(ssp103, plain, (~spl22 | spl47 | spl49 | spl57), inference(avatar_split_clause, [status(thm)], [p1148, sdef47, sdef49, sdef57])).
% 9.87/3.41  cnf(p538, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(X1,sk2),X0) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [p212, p305])).
% 9.87/3.41  cnf(p1149, plain, apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk2),X0) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [p128, p538])).
% 9.87/3.41  fof(sdef84, definition, (spl84 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk2),X0) | distinct_points(sk1,X1))), introduced(definition, [new_symbols(naming, [spl84])], [avatar_definition])).
% 9.87/3.41  cnf(ssp104, plain, (spl47 | spl49 | spl84), inference(avatar_split_clause, [status(thm)], [p1149, sdef47, sdef49, sdef84])).
% 9.87/3.41  cnf(p1151, plain, apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(X0,sk2)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p128, p538])).
% 9.87/3.41  fof(sdef85, definition, (spl85 <=> (apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk2)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl85])], [avatar_definition])).
% 9.87/3.41  cnf(ssp105, plain, (spl61 | spl85), inference(avatar_split_clause, [status(thm)], [p1151, sdef61, sdef85])).
% 9.87/3.41  cnf(p948, plain, distinct_lines(line_connecting(X0,sk2),line_connecting(sk0,sk2)) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p538, c1])).
% 9.87/3.41  cnf(p1153, plain, apart_point_and_line(sk0,line_connecting(X0,sk2)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk2)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p128, p948])).
% 9.87/3.41  cnf(ssp106, plain, (spl47 | spl49 | spl85), inference(avatar_split_clause, [status(thm)], [p1153, sdef47, sdef49, sdef85])).
% 9.87/3.41  cnf(p540, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,X1),X0) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [p212, p342])).
% 9.87/3.41  cnf(p1154, plain, apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(sk2,X0)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p128, p540])).
% 9.87/3.41  fof(sdef86, definition, (spl86 <=> (apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk2,line_connecting(sk2,X0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl86])], [avatar_definition])).
% 9.87/3.41  cnf(ssp107, plain, (spl61 | spl86), inference(avatar_split_clause, [status(thm)], [p1154, sdef61, sdef86])).
% 9.87/3.41  cnf(p953, plain, distinct_lines(line_connecting(sk0,sk2),line_connecting(sk2,X0)) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p540, c1])).
% 9.87/3.41  cnf(p1156, plain, apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk2,X0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk2,X0)) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p128, p953])).
% 9.87/3.41  cnf(ssp108, plain, (spl47 | spl49 | spl86), inference(avatar_split_clause, [status(thm)], [p1156, sdef47, sdef49, sdef86])).
% 9.87/3.41  cnf(p543, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(sk0,X1) | ~spl23), inference(avatar_component_clause, [status(thm)], [sdef23])).
% 9.87/3.41  cnf(p1157, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(sk0,X1) | ~spl23), inference(resolution, [status(thm)], [p128, p543])).
% 9.87/3.41  cnf(ssp109, plain, (~spl23 | spl47 | spl49 | spl66), inference(avatar_split_clause, [status(thm)], [p1157, sdef47, sdef49, sdef66])).
% 9.87/3.41  cnf(p1158, plain, (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_points(sk0,X0) | ~spl23), inference(resolution, [status(thm)], [p128, p543])).
% 9.87/3.41  cnf(ssp110, plain, (~spl23 | spl58 | spl61), inference(avatar_split_clause, [status(thm)], [p1158, sdef58, sdef61])).
% 9.87/3.41  cnf(p956, plain, (distinct_lines(line_connecting(X0,sk1),line_connecting(sk0,sk2)) | distinct_points(sk0,X0) | ~spl23), inference(resolution, [status(thm)], [p543, c1])).
% 9.87/3.41  cnf(p1159, plain, (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | distinct_points(sk0,X0) | ~spl23), inference(resolution, [status(thm)], [p128, p956])).
% 9.87/3.41  cnf(ssp111, plain, (~spl23 | spl47 | spl49 | spl58), inference(avatar_split_clause, [status(thm)], [p1159, sdef47, sdef49, sdef58])).
% 9.87/3.41  cnf(p545, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(X1,sk0) | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 9.87/3.41  cnf(p1160, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(X1,sk0) | ~spl24), inference(resolution, [status(thm)], [p128, p545])).
% 9.87/3.41  cnf(ssp112, plain, (~spl24 | spl47 | spl49 | spl67), inference(avatar_split_clause, [status(thm)], [p1160, sdef47, sdef49, sdef67])).
% 9.87/3.41  cnf(p1161, plain, (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_points(X0,sk0) | ~spl24), inference(resolution, [status(thm)], [p128, p545])).
% 9.87/3.41  cnf(ssp113, plain, (~spl24 | spl59 | spl61), inference(avatar_split_clause, [status(thm)], [p1161, sdef59, sdef61])).
% 9.87/3.41  cnf(p961, plain, (distinct_lines(line_connecting(X0,sk1),line_connecting(sk0,sk2)) | distinct_points(X0,sk0) | ~spl24), inference(resolution, [status(thm)], [p545, c1])).
% 9.87/3.41  cnf(p1162, plain, (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | distinct_points(X0,sk0) | ~spl24), inference(resolution, [status(thm)], [p128, p961])).
% 9.87/3.41  cnf(ssp114, plain, (~spl24 | spl47 | spl49 | spl59), inference(avatar_split_clause, [status(thm)], [p1162, sdef47, sdef49, sdef59])).
% 9.87/3.41  cnf(p547, plain, distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(X1,sk0),X0) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [p212, p393])).
% 9.87/3.41  cnf(p1163, plain, apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk0),X0) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [p128, p547])).
% 9.87/3.41  fof(sdef87, definition, (spl87 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk0),X0) | distinct_points(sk1,X1))), introduced(definition, [new_symbols(naming, [spl87])], [avatar_definition])).
% 9.87/3.41  cnf(ssp115, plain, (spl47 | spl49 | spl87), inference(avatar_split_clause, [status(thm)], [p1163, sdef47, sdef49, sdef87])).
% 9.87/3.41  cnf(p1165, plain, apart_point_and_line(sk0,line_connecting(X0,sk0)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p128, p547])).
% 9.87/3.41  fof(sdef88, definition, (spl88 <=> (apart_point_and_line(sk0,line_connecting(X0,sk0)) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl88])], [avatar_definition])).
% 9.87/3.41  cnf(ssp116, plain, (spl61 | spl88), inference(avatar_split_clause, [status(thm)], [p1165, sdef61, sdef88])).
% 9.87/3.41  cnf(p965, plain, distinct_lines(line_connecting(X0,sk0),line_connecting(sk0,sk2)) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p547, c1])).
% 9.87/3.41  cnf(p1167, plain, apart_point_and_line(sk0,line_connecting(X0,sk0)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p128, p965])).
% 9.87/3.41  cnf(ssp117, plain, (spl47 | spl49 | spl88), inference(avatar_split_clause, [status(thm)], [p1167, sdef47, sdef49, sdef88])).
% 9.87/3.41  cnf(p549, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,X1),X0) | distinct_points(X1,sk0) | ~spl25), inference(avatar_component_clause, [status(thm)], [sdef25])).
% 9.87/3.41  cnf(p1168, plain, (apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_points(X0,sk0) | ~spl25), inference(resolution, [status(thm)], [p128, p549])).
% 9.87/3.41  cnf(ssp118, plain, (~spl25 | spl60 | spl61), inference(avatar_split_clause, [status(thm)], [p1168, sdef60, sdef61])).
% 9.87/3.41  cnf(p973, plain, (distinct_lines(line_connecting(sk0,sk2),line_connecting(sk1,X0)) | distinct_points(X0,sk0) | ~spl25), inference(resolution, [status(thm)], [p549, c1])).
% 9.87/3.41  cnf(p1169, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(sk1,X0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | distinct_points(X0,sk0) | ~spl25), inference(resolution, [status(thm)], [p128, p973])).
% 9.87/3.41  cnf(ssp119, plain, (~spl25 | spl47 | spl49 | spl60), inference(avatar_split_clause, [status(thm)], [p1169, sdef47, sdef49, sdef60])).
% 9.87/3.41  cnf(p555, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(sk2,X1) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 9.87/3.41  cnf(p1170, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(X1,sk1),X0) | distinct_points(sk2,X1) | ~spl28), inference(resolution, [status(thm)], [p128, p555])).
% 9.87/3.41  cnf(ssp120, plain, (~spl28 | spl47 | spl49 | spl83), inference(avatar_split_clause, [status(thm)], [p1170, sdef47, sdef49, sdef83])).
% 9.87/3.41  cnf(p1171, plain, (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_points(sk2,X0) | ~spl28), inference(resolution, [status(thm)], [p128, p555])).
% 9.87/3.41  cnf(ssp121, plain, (~spl28 | spl61 | spl63), inference(avatar_split_clause, [status(thm)], [p1171, sdef61, sdef63])).
% 9.87/3.41  cnf(p975, plain, (distinct_lines(line_connecting(X0,sk1),line_connecting(sk0,sk2)) | distinct_points(sk2,X0) | ~spl28), inference(resolution, [status(thm)], [p555, c1])).
% 9.87/3.41  cnf(p1172, plain, (apart_point_and_line(sk0,line_connecting(X0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | distinct_points(sk2,X0) | ~spl28), inference(resolution, [status(thm)], [p128, p975])).
% 9.87/3.41  cnf(ssp122, plain, (~spl28 | spl47 | spl49 | spl63), inference(avatar_split_clause, [status(thm)], [p1172, sdef47, sdef49, sdef63])).
% 9.87/3.41  cnf(p1173, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk2),X1) | distinct_lines(X0,X1) | ~spl17), inference(resolution, [status(thm)], [p128, p560])).
% 9.87/3.41  cnf(ssp123, plain, (~spl17 | spl47 | spl49 | spl68), inference(avatar_split_clause, [status(thm)], [p1173, sdef47, sdef49, sdef68])).
% 9.87/3.41  cnf(p1174, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl17), inference(resolution, [status(thm)], [p128, p560])).
% 9.87/3.41  cnf(ssp124, plain, (~spl17 | spl40 | spl51 | spl69), inference(avatar_split_clause, [status(thm)], [p1174, sdef40, sdef51, sdef69])).
% 9.87/3.41  cnf(p1175, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk2),X1) | ~spl17), inference(resolution, [status(thm)], [p128, p560])).
% 9.87/3.41  cnf(ssp125, plain, (~spl17 | spl61 | spl70), inference(avatar_split_clause, [status(thm)], [p1175, sdef61, sdef70])).
% 9.87/3.41  cnf(p979, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(X0,line_connecting(sk1,sk2)) | ~spl17), inference(resolution, [status(thm)], [p560, c1])).
% 9.87/3.41  cnf(p1176, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk1,sk2)) | ~spl17), inference(resolution, [status(thm)], [p128, p979])).
% 9.87/3.41  cnf(ssp126, plain, (~spl17 | spl47 | spl49 | spl71), inference(avatar_split_clause, [status(thm)], [p1176, sdef47, sdef49, sdef71])).
% 9.87/3.41  cnf(p1177, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk1,sk0),X1) | distinct_lines(X0,X1) | ~spl18), inference(resolution, [status(thm)], [p128, p562])).
% 9.87/3.41  cnf(ssp127, plain, (~spl18 | spl47 | spl49 | spl72), inference(avatar_split_clause, [status(thm)], [p1177, sdef47, sdef49, sdef72])).
% 9.87/3.41  cnf(p1178, plain, (apart_point_and_line(sk0,line_connecting(sk1,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl18), inference(resolution, [status(thm)], [p128, p562])).
% 9.87/3.41  cnf(ssp128, plain, (~spl18 | spl43 | spl52 | spl69), inference(avatar_split_clause, [status(thm)], [p1178, sdef43, sdef52, sdef69])).
% 9.87/3.41  cnf(p1179, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk1,sk0),X1) | ~spl18), inference(resolution, [status(thm)], [p128, p562])).
% 9.87/3.41  cnf(ssp129, plain, (~spl18 | spl61 | spl73), inference(avatar_split_clause, [status(thm)], [p1179, sdef61, sdef73])).
% 9.87/3.41  cnf(p984, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(X0,line_connecting(sk1,sk0)) | ~spl18), inference(resolution, [status(thm)], [p562, c1])).
% 9.87/3.41  cnf(p1180, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk1,sk0)) | ~spl18), inference(resolution, [status(thm)], [p128, p984])).
% 9.87/3.41  cnf(ssp130, plain, (~spl18 | spl47 | spl49 | spl74), inference(avatar_split_clause, [status(thm)], [p1180, sdef47, sdef49, sdef74])).
% 9.87/3.41  cnf(p564, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X0,X1) | ~spl19), inference(resolution, [status(thm)], [p529, c4])).
% 9.87/3.41  cnf(p1181, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X0,X1) | ~spl19), inference(resolution, [status(thm)], [p128, p564])).
% 9.87/3.41  cnf(ssp131, plain, (~spl19 | spl53 | spl54 | spl75), inference(avatar_split_clause, [status(thm)], [p1181, sdef53, sdef54, sdef75])).
% 9.87/3.41  cnf(p1182, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X1,X0) | ~spl19), inference(resolution, [status(thm)], [p128, p564])).
% 9.87/3.41  cnf(ssp132, plain, (~spl19 | spl47 | spl49 | spl76), inference(avatar_split_clause, [status(thm)], [p1182, sdef47, sdef49, sdef76])).
% 9.87/3.41  cnf(p1183, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X1) | ~spl19), inference(resolution, [status(thm)], [p128, p564])).
% 9.87/3.41  cnf(ssp133, plain, (~spl19 | spl61 | spl62), inference(avatar_split_clause, [status(thm)], [p1183, sdef61, sdef62])).
% 9.87/3.41  cnf(p989, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(X0,line_connecting(sk0,sk2)) | ~spl19), inference(resolution, [status(thm)], [p564, c1])).
% 9.87/3.41  cnf(p1184, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk0,sk2)) | ~spl19), inference(resolution, [status(thm)], [p128, p989])).
% 9.87/3.41  cnf(ssp134, plain, (~spl19 | spl53 | spl54 | spl77), inference(avatar_split_clause, [status(thm)], [p1184, sdef53, sdef54, sdef77])).
% 9.87/3.41  cnf(p1185, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk2,sk1),X1) | distinct_lines(X0,X1) | ~spl20), inference(resolution, [status(thm)], [p128, p566])).
% 9.87/3.41  cnf(ssp135, plain, (~spl20 | spl47 | spl49 | spl78), inference(avatar_split_clause, [status(thm)], [p1185, sdef47, sdef49, sdef78])).
% 9.87/3.41  cnf(p1186, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl20), inference(resolution, [status(thm)], [p128, p566])).
% 9.87/3.41  cnf(ssp136, plain, (~spl20 | spl45 | spl55 | spl69), inference(avatar_split_clause, [status(thm)], [p1186, sdef45, sdef55, sdef69])).
% 9.87/3.41  cnf(p1187, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(line_connecting(sk2,sk1),X1) | ~spl20), inference(resolution, [status(thm)], [p128, p566])).
% 9.87/3.41  cnf(ssp137, plain, (~spl20 | spl61 | spl79), inference(avatar_split_clause, [status(thm)], [p1187, sdef61, sdef79])).
% 9.87/3.41  cnf(p995, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl20), inference(resolution, [status(thm)], [p566, c1])).
% 9.87/3.41  cnf(p1188, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl20), inference(resolution, [status(thm)], [p128, p995])).
% 9.87/3.41  cnf(ssp138, plain, (~spl20 | spl47 | spl49 | spl80), inference(avatar_split_clause, [status(thm)], [p1188, sdef47, sdef49, sdef80])).
% 9.87/3.41  cnf(p568, plain, (distinct_points(sk1,X0) | distinct_points(sk2,X1) | distinct_lines(line_connecting(sk0,sk2),line_connecting(X0,X1)) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 9.87/3.41  cnf(p1189, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,line_connecting(X0,X1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,X1)) | distinct_points(sk1,X0) | distinct_points(sk2,X1) | ~spl29), inference(resolution, [status(thm)], [p128, p568])).
% 9.87/3.41  fof(sdef89, definition, (spl89 <=> (apart_point_and_line(sk0,line_connecting(X0,X1)) | apart_point_and_line(sk2,line_connecting(X0,X1)) | distinct_points(sk1,X0) | distinct_points(sk2,X1))), introduced(definition, [new_symbols(naming, [spl89])], [avatar_definition])).
% 9.87/3.41  cnf(ssp139, plain, (~spl29 | spl47 | spl49 | spl89), inference(avatar_split_clause, [status(thm)], [p1189, sdef47, sdef49, sdef89])).
% 9.87/3.41  cnf(p129, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1), inference(resolution, [status(thm)], [c10, c16])).
% 9.87/3.41  cnf(p1198, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl0), inference(resolution, [status(thm)], [p129, p508])).
% 9.87/3.41  fof(sdef90, definition, (spl90 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl90])], [avatar_definition])).
% 9.87/3.41  cnf(ssp140, plain, (~spl0 | spl42 | spl51 | spl90), inference(avatar_split_clause, [status(thm)], [p1198, sdef42, sdef51, sdef90])).
% 9.87/3.41  cnf(p1200, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl2), inference(resolution, [status(thm)], [p129, p510])).
% 9.87/3.41  cnf(ssp141, plain, (~spl2 | spl44 | spl52 | spl90), inference(avatar_split_clause, [status(thm)], [p1200, sdef44, sdef52, sdef90])).
% 9.87/3.41  cnf(p1201, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl4), inference(resolution, [status(thm)], [p129, p513])).
% 9.87/3.41  cnf(ssp142, plain, (~spl4 | spl46 | spl55 | spl90), inference(avatar_split_clause, [status(thm)], [p1201, sdef46, sdef55, sdef90])).
% 9.87/3.41  cnf(p1202, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl17), inference(resolution, [status(thm)], [p129, p560])).
% 9.87/3.41  cnf(ssp143, plain, (~spl17 | spl42 | spl51 | spl90), inference(avatar_split_clause, [status(thm)], [p1202, sdef42, sdef51, sdef90])).
% 9.87/3.41  cnf(p1203, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl18), inference(resolution, [status(thm)], [p129, p562])).
% 9.87/3.41  cnf(ssp144, plain, (~spl18 | spl44 | spl52 | spl90), inference(avatar_split_clause, [status(thm)], [p1203, sdef44, sdef52, sdef90])).
% 9.87/3.41  cnf(p1204, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl20), inference(resolution, [status(thm)], [p129, p566])).
% 9.87/3.41  cnf(ssp145, plain, (~spl20 | spl46 | spl55 | spl90), inference(avatar_split_clause, [status(thm)], [p1204, sdef46, sdef55, sdef90])).
% 9.87/3.41  cnf(p130, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(sk0,X2), inference(resolution, [status(thm)], [c10, p19])).
% 9.87/3.41  cnf(p1213, 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,sk2),X2) | distinct_lines(X2,X0) | ~spl0), inference(resolution, [status(thm)], [p130, p508])).
% 9.87/3.41  fof(sdef91, definition, (spl91 <=> (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,sk2),X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl91])], [avatar_definition])).
% 9.87/3.41  cnf(ssp146, plain, (~spl0 | spl42 | spl91), inference(avatar_split_clause, [status(thm)], [p1213, sdef42, sdef91])).
% 9.87/3.41  cnf(p1215, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk1,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X2,X0) | ~spl2), inference(resolution, [status(thm)], [p130, p510])).
% 9.87/3.41  fof(sdef92, definition, (spl92 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk1,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl92])], [avatar_definition])).
% 9.87/3.41  cnf(ssp147, plain, (~spl2 | spl44 | spl92), inference(avatar_split_clause, [status(thm)], [p1215, sdef44, sdef92])).
% 9.87/3.41  cnf(p1217, 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,sk2),X2) | distinct_lines(X2,X0) | ~spl4), inference(resolution, [status(thm)], [p130, p513])).
% 9.87/3.41  fof(sdef93, definition, (spl93 <=> (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,sk2),X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl93])], [avatar_definition])).
% 9.87/3.41  cnf(ssp148, plain, (~spl4 | spl46 | spl93), inference(avatar_split_clause, [status(thm)], [p1217, sdef46, sdef93])).
% 9.87/3.41  cnf(p1219, 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,sk2),X2) | distinct_lines(X2,X0) | ~spl17), inference(resolution, [status(thm)], [p130, p560])).
% 9.87/3.41  cnf(ssp149, plain, (~spl17 | spl42 | spl91), inference(avatar_split_clause, [status(thm)], [p1219, sdef42, sdef91])).
% 9.87/3.41  cnf(p1220, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk1,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X2,X0) | ~spl18), inference(resolution, [status(thm)], [p130, p562])).
% 9.87/3.41  cnf(ssp150, plain, (~spl18 | spl44 | spl92), inference(avatar_split_clause, [status(thm)], [p1220, sdef44, sdef92])).
% 9.87/3.41  cnf(p1221, 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,sk2),X2) | distinct_lines(X2,X0) | ~spl20), inference(resolution, [status(thm)], [p130, p566])).
% 9.87/3.41  cnf(ssp151, plain, (~spl20 | spl46 | spl93), inference(avatar_split_clause, [status(thm)], [p1221, sdef46, sdef93])).
% 9.87/3.41  cnf(p20, plain, distinct_points(sk0,X0) | distinct_points(sk2,X0), inference(resolution, [status(thm)], [c3, c15])).
% 9.87/3.41  cnf(p131, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(sk0,X2), inference(resolution, [status(thm)], [c10, p20])).
% 9.87/3.41  cnf(p1230, plain, apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | apart_point_and_line(sk1,X0), inference(resolution, [status(thm)], [p131, p204])).
% 9.87/3.41  fof(sdef94, definition, (spl94 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | apart_point_and_line(sk1,X0))), introduced(definition, [new_symbols(naming, [spl94])], [avatar_definition])).
% 9.87/3.41  cnf(ssp152, plain, (spl49 | spl94), inference(avatar_split_clause, [status(thm)], [p1230, sdef49, sdef94])).
% 9.87/3.41  cnf(p1232, plain, apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | apart_point_and_line(X2,X0) | distinct_points(sk1,X2), inference(resolution, [status(thm)], [p131, p205])).
% 9.87/3.41  fof(sdef95, definition, (spl95 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | apart_point_and_line(X2,X0) | distinct_points(sk1,X2))), introduced(definition, [new_symbols(naming, [spl95])], [avatar_definition])).
% 9.87/3.41  cnf(ssp153, plain, (spl49 | spl95), inference(avatar_split_clause, [status(thm)], [p1232, sdef49, sdef95])).
% 9.87/3.41  cnf(p1234, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk0,X0) | ~spl0), inference(resolution, [status(thm)], [p131, p451])).
% 9.87/3.41  fof(sdef96, definition, (spl96 <=> (apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl96])], [avatar_definition])).
% 9.87/3.41  cnf(ssp154, plain, (~spl0 | spl49 | spl51 | spl96), inference(avatar_split_clause, [status(thm)], [p1234, sdef49, sdef51, sdef96])).
% 9.87/3.41  cnf(p1236, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk1,sk0)) | distinct_points(sk0,X0) | ~spl2), inference(resolution, [status(thm)], [p131, p454])).
% 9.87/3.41  fof(sdef97, definition, (spl97 <=> (apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk1,sk0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl97])], [avatar_definition])).
% 9.87/3.41  cnf(ssp155, plain, (~spl2 | spl49 | spl52 | spl97), inference(avatar_split_clause, [status(thm)], [p1236, sdef49, sdef52, sdef97])).
% 9.87/3.41  cnf(p1238, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(sk0,X0) | ~spl3), inference(resolution, [status(thm)], [p131, p456])).
% 9.87/3.41  fof(sdef98, definition, (spl98 <=> (apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl98])], [avatar_definition])).
% 9.87/3.41  cnf(ssp156, plain, (~spl3 | spl49 | spl54 | spl98), inference(avatar_split_clause, [status(thm)], [p1238, sdef49, sdef54, sdef98])).
% 9.87/3.41  cnf(p1240, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk0,X0) | ~spl4), inference(resolution, [status(thm)], [p131, p458])).
% 9.87/3.41  fof(sdef99, definition, (spl99 <=> (apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl99])], [avatar_definition])).
% 9.87/3.41  cnf(ssp157, plain, (~spl4 | spl49 | spl55 | spl99), inference(avatar_split_clause, [status(thm)], [p1240, sdef49, sdef55, sdef99])).
% 9.87/3.41  cnf(p1242, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(sk0,X0) | ~spl5), inference(resolution, [status(thm)], [p131, p461])).
% 9.87/3.41  fof(sdef100, definition, (spl100 <=> (apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl100])], [avatar_definition])).
% 9.87/3.41  cnf(ssp158, plain, (~spl5 | spl49 | spl100), inference(avatar_split_clause, [status(thm)], [p1242, sdef49, sdef100])).
% 9.87/3.41  cnf(p1244, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(X0,sk2) | ~spl6), inference(resolution, [status(thm)], [p131, p463])).
% 9.87/3.41  fof(sdef101, definition, (spl101 <=> (apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(X0,sk2))), introduced(definition, [new_symbols(naming, [spl101])], [avatar_definition])).
% 9.87/3.41  cnf(ssp159, plain, (~spl6 | spl49 | spl101), inference(avatar_split_clause, [status(thm)], [p1244, sdef49, sdef101])).
% 9.87/3.41  cnf(p1246, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(sk0,X1) | distinct_points(sk0,X0) | ~spl10), inference(resolution, [status(thm)], [p131, p473])).
% 9.87/3.41  fof(sdef102, definition, (spl102 <=> (apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(sk0,X1) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl102])], [avatar_definition])).
% 9.87/3.41  cnf(ssp160, plain, (~spl10 | spl49 | spl102), inference(avatar_split_clause, [status(thm)], [p1246, sdef49, sdef102])).
% 9.87/3.41  cnf(p1248, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(sk0,X1) | distinct_points(X0,sk0) | ~spl11), inference(resolution, [status(thm)], [p131, p475])).
% 9.87/3.41  fof(sdef103, definition, (spl103 <=> (apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(sk0,X1) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl103])], [avatar_definition])).
% 9.87/3.41  cnf(ssp161, plain, (~spl11 | spl49 | spl103), inference(avatar_split_clause, [status(thm)], [p1248, sdef49, sdef103])).
% 9.87/3.41  cnf(p1250, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(X0,sk0) | ~spl13), inference(resolution, [status(thm)], [p131, p481])).
% 9.87/3.41  fof(sdef104, definition, (spl104 <=> (apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl104])], [avatar_definition])).
% 9.87/3.41  cnf(ssp162, plain, (~spl13 | spl49 | spl104), inference(avatar_split_clause, [status(thm)], [p1250, sdef49, sdef104])).
% 9.87/3.41  cnf(p1252, plain, (apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,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,sk2),X0) | ~spl0), inference(resolution, [status(thm)], [p131, p485])).
% 9.87/3.41  fof(sdef105, definition, (spl105 <=> (apart_point_and_line(sk2,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,sk2),X0))), introduced(definition, [new_symbols(naming, [spl105])], [avatar_definition])).
% 9.87/3.41  cnf(ssp163, plain, (~spl0 | spl51 | spl105), inference(avatar_split_clause, [status(thm)], [p1252, sdef51, sdef105])).
% 9.87/3.41  cnf(p1254, plain, (apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk1,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl2), inference(resolution, [status(thm)], [p131, p497])).
% 9.87/3.41  fof(sdef106, definition, (spl106 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk1,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X0))), introduced(definition, [new_symbols(naming, [spl106])], [avatar_definition])).
% 9.87/3.41  cnf(ssp164, plain, (~spl2 | spl52 | spl106), inference(avatar_split_clause, [status(thm)], [p1254, sdef52, sdef106])).
% 9.87/3.41  cnf(p1256, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,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) | ~spl3), inference(resolution, [status(thm)], [p131, p498])).
% 9.87/3.41  fof(sdef107, definition, (spl107 <=> (apart_point_and_line(sk2,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, [spl107])], [avatar_definition])).
% 9.87/3.41  cnf(ssp165, plain, (~spl3 | spl49 | spl107), inference(avatar_split_clause, [status(thm)], [p1256, sdef49, sdef107])).
% 9.87/3.41  cnf(p1258, plain, (apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,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,sk2),X0) | ~spl4), inference(resolution, [status(thm)], [p131, p499])).
% 9.87/3.41  fof(sdef108, definition, (spl108 <=> (apart_point_and_line(sk2,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,sk2),X0))), introduced(definition, [new_symbols(naming, [spl108])], [avatar_definition])).
% 9.87/3.41  cnf(ssp166, plain, (~spl4 | spl55 | spl108), inference(avatar_split_clause, [status(thm)], [p1258, sdef55, sdef108])).
% 9.87/3.41  cnf(p1260, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(sk0,X1) | distinct_points(sk2,X0) | ~spl16), inference(resolution, [status(thm)], [p131, p518])).
% 9.87/3.41  fof(sdef109, definition, (spl109 <=> (apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | distinct_points(sk0,X1) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl109])], [avatar_definition])).
% 9.87/3.41  cnf(ssp167, plain, (~spl16 | spl49 | spl109), inference(avatar_split_clause, [status(thm)], [p1260, sdef49, sdef109])).
% 9.87/3.41  cnf(p1262, plain, apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | apart_point_and_line(sk1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p131, p212])).
% 9.87/3.41  fof(sdef110, definition, (spl110 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | apart_point_and_line(sk1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl110])], [avatar_definition])).
% 9.87/3.41  cnf(ssp168, plain, (spl49 | spl110), inference(avatar_split_clause, [status(thm)], [p1262, sdef49, sdef110])).
% 9.87/3.41  cnf(p1265, plain, (apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,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,sk2),X0) | ~spl17), inference(resolution, [status(thm)], [p131, p525])).
% 9.87/3.41  cnf(ssp169, plain, (~spl17 | spl51 | spl105), inference(avatar_split_clause, [status(thm)], [p1265, sdef51, sdef105])).
% 9.87/3.41  cnf(p1266, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk0,X0) | ~spl17), inference(resolution, [status(thm)], [p131, p559])).
% 9.87/3.41  cnf(ssp170, plain, (~spl17 | spl49 | spl51 | spl96), inference(avatar_split_clause, [status(thm)], [p1266, sdef49, sdef51, sdef96])).
% 9.87/3.41  cnf(p1267, plain, (apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk1,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl18), inference(resolution, [status(thm)], [p131, p527])).
% 9.87/3.41  cnf(ssp171, plain, (~spl18 | spl52 | spl106), inference(avatar_split_clause, [status(thm)], [p1267, sdef52, sdef106])).
% 9.87/3.41  cnf(p1268, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk1,sk0)) | distinct_points(sk0,X0) | ~spl18), inference(resolution, [status(thm)], [p131, p561])).
% 9.87/3.41  cnf(ssp172, plain, (~spl18 | spl49 | spl52 | spl97), inference(avatar_split_clause, [status(thm)], [p1268, sdef49, sdef52, sdef97])).
% 9.87/3.41  cnf(p1269, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,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) | ~spl19), inference(resolution, [status(thm)], [p131, p529])).
% 9.87/3.41  cnf(ssp173, plain, (~spl19 | spl49 | spl107), inference(avatar_split_clause, [status(thm)], [p1269, sdef49, sdef107])).
% 9.87/3.41  cnf(p1270, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,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) | ~spl19), inference(resolution, [status(thm)], [p131, p563])).
% 9.87/3.41  cnf(ssp174, plain, (~spl19 | spl49 | spl54 | spl98), inference(avatar_split_clause, [status(thm)], [p1270, sdef49, sdef54, sdef98])).
% 9.87/3.41  cnf(p1271, plain, (apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,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,sk2),X0) | ~spl20), inference(resolution, [status(thm)], [p131, p531])).
% 9.87/3.41  cnf(ssp175, plain, (~spl20 | spl55 | spl108), inference(avatar_split_clause, [status(thm)], [p1271, sdef55, sdef108])).
% 9.87/3.41  cnf(p1272, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk0,X0) | ~spl20), inference(resolution, [status(thm)], [p131, p565])).
% 9.87/3.41  cnf(ssp176, plain, (~spl20 | spl49 | spl55 | spl99), inference(avatar_split_clause, [status(thm)], [p1272, sdef49, sdef55, sdef99])).
% 9.87/3.41  cnf(p1273, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(sk0,X2) | distinct_points(X2,X0) | ~spl14), inference(resolution, [status(thm)], [p131, p483])).
% 9.87/3.41  fof(sdef111, definition, (spl111 <=> (apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(sk0,X2) | distinct_points(X2,X0))), introduced(definition, [new_symbols(naming, [spl111])], [avatar_definition])).
% 9.87/3.41  cnf(ssp177, plain, (~spl14 | spl49 | spl111), inference(avatar_split_clause, [status(thm)], [p1273, sdef49, sdef111])).
% 9.87/3.41  cnf(p1275, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(sk0,X0) | ~spl14), inference(resolution, [status(thm)], [p131, p872])).
% 9.87/3.41  cnf(ssp178, plain, (~spl14 | spl49 | spl100), inference(avatar_split_clause, [status(thm)], [p1275, sdef49, sdef100])).
% 9.87/3.41  cnf(p1278, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_points(sk0,X2) | distinct_lines(line_connecting(X2,sk1),X0) | ~spl10), inference(resolution, [status(thm)], [p131, p504])).
% 9.87/3.41  fof(sdef112, definition, (spl112 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_points(sk0,X2) | distinct_lines(line_connecting(X2,sk1),X0))), introduced(definition, [new_symbols(naming, [spl112])], [avatar_definition])).
% 9.87/3.41  cnf(ssp179, plain, (~spl10 | spl49 | spl112), inference(avatar_split_clause, [status(thm)], [p1278, sdef49, sdef112])).
% 9.87/3.41  cnf(p1281, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_points(X2,sk0) | distinct_lines(line_connecting(X2,sk1),X0) | ~spl11), inference(resolution, [status(thm)], [p131, p505])).
% 9.87/3.41  fof(sdef113, definition, (spl113 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_points(X2,sk0) | distinct_lines(line_connecting(X2,sk1),X0))), introduced(definition, [new_symbols(naming, [spl113])], [avatar_definition])).
% 9.87/3.41  cnf(ssp180, plain, (~spl11 | spl49 | spl113), inference(avatar_split_clause, [status(thm)], [p1281, sdef49, sdef113])).
% 9.87/3.41  cnf(p1285, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk1,sk2),X2) | distinct_lines(X0,X2) | ~spl0), inference(resolution, [status(thm)], [p131, p508])).
% 9.87/3.41  fof(sdef114, definition, (spl114 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk1,sk2),X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl114])], [avatar_definition])).
% 9.87/3.41  cnf(ssp181, plain, (~spl0 | spl49 | spl114), inference(avatar_split_clause, [status(thm)], [p1285, sdef49, sdef114])).
% 9.87/3.41  cnf(p1287, plain, (apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,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,sk2),X2) | distinct_lines(X2,X0) | ~spl0), inference(resolution, [status(thm)], [p131, p508])).
% 9.87/3.41  fof(sdef115, definition, (spl115 <=> (apart_point_and_line(sk2,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,sk2),X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl115])], [avatar_definition])).
% 9.87/3.41  cnf(ssp182, plain, (~spl0 | spl51 | spl115), inference(avatar_split_clause, [status(thm)], [p1287, sdef51, sdef115])).
% 9.87/3.41  cnf(p1290, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk1,sk2)) | ~spl0), inference(resolution, [status(thm)], [p131, p904])).
% 9.87/3.41  fof(sdef116, definition, (spl116 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl116])], [avatar_definition])).
% 9.87/3.41  cnf(ssp183, plain, (~spl0 | spl49 | spl116), inference(avatar_split_clause, [status(thm)], [p1290, sdef49, sdef116])).
% 9.87/3.41  cnf(p1292, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk1,sk0),X2) | distinct_lines(X0,X2) | ~spl2), inference(resolution, [status(thm)], [p131, p510])).
% 9.87/3.41  fof(sdef117, definition, (spl117 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk1,sk0),X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl117])], [avatar_definition])).
% 9.87/3.41  cnf(ssp184, plain, (~spl2 | spl49 | spl117), inference(avatar_split_clause, [status(thm)], [p1292, sdef49, sdef117])).
% 9.87/3.41  cnf(p1294, plain, (apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk1,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X2,X0) | ~spl2), inference(resolution, [status(thm)], [p131, p510])).
% 9.87/3.41  fof(sdef118, definition, (spl118 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk1,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl118])], [avatar_definition])).
% 9.87/3.41  cnf(ssp185, plain, (~spl2 | spl52 | spl118), inference(avatar_split_clause, [status(thm)], [p1294, sdef52, sdef118])).
% 9.87/3.41  cnf(p1297, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk1,sk0)) | ~spl2), inference(resolution, [status(thm)], [p131, p910])).
% 9.87/3.41  fof(sdef119, definition, (spl119 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk1,sk0)))), introduced(definition, [new_symbols(naming, [spl119])], [avatar_definition])).
% 9.87/3.41  cnf(ssp186, plain, (~spl2 | spl49 | spl119), inference(avatar_split_clause, [status(thm)], [p1297, sdef49, sdef119])).
% 9.87/3.41  cnf(p1299, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X0,X2) | ~spl3), inference(resolution, [status(thm)], [p131, p512])).
% 9.87/3.41  fof(sdef120, definition, (spl120 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl120])], [avatar_definition])).
% 9.87/3.41  cnf(ssp187, plain, (~spl3 | spl54 | spl120), inference(avatar_split_clause, [status(thm)], [p1299, sdef54, sdef120])).
% 9.87/3.41  cnf(p1301, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,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),X2) | distinct_lines(X2,X0) | ~spl3), inference(resolution, [status(thm)], [p131, p512])).
% 9.87/3.41  fof(sdef121, definition, (spl121 <=> (apart_point_and_line(sk2,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),X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl121])], [avatar_definition])).
% 9.87/3.41  cnf(ssp188, plain, (~spl3 | spl49 | spl121), inference(avatar_split_clause, [status(thm)], [p1301, sdef49, sdef121])).
% 9.87/3.41  cnf(p1304, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk0,sk2)) | ~spl3), inference(resolution, [status(thm)], [p131, p915])).
% 9.87/3.41  fof(sdef122, definition, (spl122 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl122])], [avatar_definition])).
% 9.87/3.41  cnf(ssp189, plain, (~spl3 | spl54 | spl122), inference(avatar_split_clause, [status(thm)], [p1304, sdef54, sdef122])).
% 9.87/3.41  cnf(p1306, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk2,sk1),X2) | distinct_lines(X0,X2) | ~spl4), inference(resolution, [status(thm)], [p131, p513])).
% 9.87/3.41  fof(sdef123, definition, (spl123 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk2,sk1),X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl123])], [avatar_definition])).
% 9.87/3.41  cnf(ssp190, plain, (~spl4 | spl49 | spl123), inference(avatar_split_clause, [status(thm)], [p1306, sdef49, sdef123])).
% 9.87/3.41  cnf(p1308, plain, (apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,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,sk2),X2) | distinct_lines(X2,X0) | ~spl4), inference(resolution, [status(thm)], [p131, p513])).
% 9.87/3.41  fof(sdef124, definition, (spl124 <=> (apart_point_and_line(sk2,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,sk2),X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl124])], [avatar_definition])).
% 9.87/3.41  cnf(ssp191, plain, (~spl4 | spl55 | spl124), inference(avatar_split_clause, [status(thm)], [p1308, sdef55, sdef124])).
% 9.87/3.41  cnf(p1311, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl4), inference(resolution, [status(thm)], [p131, p920])).
% 9.87/3.41  fof(sdef125, definition, (spl125 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl125])], [avatar_definition])).
% 9.87/3.41  cnf(ssp192, plain, (~spl4 | spl49 | spl125), inference(avatar_split_clause, [status(thm)], [p1311, sdef49, sdef125])).
% 9.87/3.41  cnf(p1313, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(sk2,X2) | distinct_points(X0,X2) | ~spl15), inference(resolution, [status(thm)], [p131, p515])).
% 9.87/3.41  fof(sdef126, definition, (spl126 <=> (apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(sk2,X2) | distinct_points(X0,X2))), introduced(definition, [new_symbols(naming, [spl126])], [avatar_definition])).
% 9.87/3.41  cnf(ssp193, plain, (~spl15 | spl49 | spl126), inference(avatar_split_clause, [status(thm)], [p1313, sdef49, sdef126])).
% 9.87/3.41  cnf(p1315, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(X0,sk2) | ~spl15), inference(resolution, [status(thm)], [p131, p927])).
% 9.87/3.41  cnf(ssp194, plain, (~spl15 | spl49 | spl101), inference(avatar_split_clause, [status(thm)], [p1315, sdef49, sdef101])).
% 9.87/3.41  cnf(p1316, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(sk2,X0) | ~spl15), inference(resolution, [status(thm)], [p131, p928])).
% 9.87/3.41  fof(sdef127, definition, (spl127 <=> (apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl127])], [avatar_definition])).
% 9.87/3.41  cnf(ssp195, plain, (~spl15 | spl49 | spl127), inference(avatar_split_clause, [status(thm)], [p1316, sdef49, sdef127])).
% 9.87/3.41  cnf(p1318, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_points(sk2,X2) | distinct_lines(line_connecting(X2,sk1),X0) | ~spl16), inference(resolution, [status(thm)], [p131, p519])).
% 9.87/3.41  fof(sdef128, definition, (spl128 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_points(sk2,X2) | distinct_lines(line_connecting(X2,sk1),X0))), introduced(definition, [new_symbols(naming, [spl128])], [avatar_definition])).
% 9.87/3.41  cnf(ssp196, plain, (~spl16 | spl49 | spl128), inference(avatar_split_clause, [status(thm)], [p1318, sdef49, sdef128])).
% 9.87/3.41  cnf(p1322, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(sk0,X0) | ~spl21), inference(resolution, [status(thm)], [p131, p944])).
% 9.87/3.41  cnf(ssp197, plain, (~spl21 | spl49 | spl100), inference(avatar_split_clause, [status(thm)], [p1322, sdef49, sdef100])).
% 9.87/3.41  cnf(p1324, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(X0,sk2) | ~spl22), inference(resolution, [status(thm)], [p131, p946])).
% 9.87/3.41  cnf(ssp198, plain, (~spl22 | spl49 | spl101), inference(avatar_split_clause, [status(thm)], [p1324, sdef49, sdef101])).
% 9.87/3.41  cnf(p1325, plain, apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(X2,sk2),X0) | distinct_points(sk1,X2), inference(resolution, [status(thm)], [p131, p538])).
% 9.87/3.41  fof(sdef129, definition, (spl129 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(X2,sk2),X0) | distinct_points(sk1,X2))), introduced(definition, [new_symbols(naming, [spl129])], [avatar_definition])).
% 9.87/3.41  cnf(ssp199, plain, (spl49 | spl129), inference(avatar_split_clause, [status(thm)], [p1325, sdef49, sdef129])).
% 9.87/3.41  cnf(p1328, plain, apart_point_and_line(sk2,line_connecting(X0,sk2)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p131, p948])).
% 9.87/3.41  fof(sdef130, definition, (spl130 <=> (apart_point_and_line(sk2,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(X0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl130])], [avatar_definition])).
% 9.87/3.41  cnf(ssp200, plain, (spl49 | spl130), inference(avatar_split_clause, [status(thm)], [p1328, sdef49, sdef130])).
% 9.87/3.41  cnf(p1331, plain, apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk0,X1) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p131, p953])).
% 9.87/3.41  fof(sdef131, definition, (spl131 <=> (apart_point_and_line(sk2,line_connecting(sk2,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk2,X0)) | distinct_points(sk0,X1) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl131])], [avatar_definition])).
% 9.87/3.41  cnf(ssp201, plain, (spl49 | spl131), inference(avatar_split_clause, [status(thm)], [p1331, sdef49, sdef131])).
% 9.87/3.41  cnf(p1333, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(X2,sk1),X0) | distinct_points(sk0,X2) | ~spl23), inference(resolution, [status(thm)], [p131, p543])).
% 9.87/3.41  cnf(ssp202, plain, (~spl23 | spl49 | spl112), inference(avatar_split_clause, [status(thm)], [p1333, sdef49, sdef112])).
% 9.87/3.41  cnf(p1335, plain, (apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_points(sk0,X0) | ~spl23), inference(resolution, [status(thm)], [p131, p956])).
% 9.87/3.41  cnf(ssp203, plain, (~spl23 | spl49 | spl102), inference(avatar_split_clause, [status(thm)], [p1335, sdef49, sdef102])).
% 9.87/3.41  cnf(p1336, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(X2,sk1),X0) | distinct_points(X2,sk0) | ~spl24), inference(resolution, [status(thm)], [p131, p545])).
% 9.87/3.41  cnf(ssp204, plain, (~spl24 | spl49 | spl113), inference(avatar_split_clause, [status(thm)], [p1336, sdef49, sdef113])).
% 9.87/3.41  cnf(p1338, plain, (apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_points(X0,sk0) | ~spl24), inference(resolution, [status(thm)], [p131, p961])).
% 9.87/3.41  cnf(ssp205, plain, (~spl24 | spl49 | spl103), inference(avatar_split_clause, [status(thm)], [p1338, sdef49, sdef103])).
% 9.87/3.41  cnf(p1339, plain, apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(X2,sk0),X0) | distinct_points(sk1,X2), inference(resolution, [status(thm)], [p131, p547])).
% 9.87/3.41  fof(sdef132, definition, (spl132 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(X2,sk0),X0) | distinct_points(sk1,X2))), introduced(definition, [new_symbols(naming, [spl132])], [avatar_definition])).
% 9.87/3.41  cnf(ssp206, plain, (spl49 | spl132), inference(avatar_split_clause, [status(thm)], [p1339, sdef49, sdef132])).
% 9.87/3.41  cnf(p1342, plain, apart_point_and_line(sk2,line_connecting(X0,sk0)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(X0,sk0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p131, p965])).
% 9.87/3.41  fof(sdef133, definition, (spl133 <=> (apart_point_and_line(sk2,line_connecting(X0,sk0)) | apart_point_and_line(X1,line_connecting(X0,sk0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl133])], [avatar_definition])).
% 9.87/3.41  cnf(ssp207, plain, (spl49 | spl133), inference(avatar_split_clause, [status(thm)], [p1342, sdef49, sdef133])).
% 9.87/3.41  cnf(p1345, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(sk1,X0)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk1,X0)) | distinct_points(sk0,X1) | distinct_points(X0,sk0) | ~spl25), inference(resolution, [status(thm)], [p131, p973])).
% 9.87/3.41  cnf(ssp208, plain, (~spl25 | spl49 | spl104), inference(avatar_split_clause, [status(thm)], [p1345, sdef49, sdef104])).
% 9.87/3.41  cnf(p1346, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(X2,sk1),X0) | distinct_points(sk2,X2) | ~spl28), inference(resolution, [status(thm)], [p131, p555])).
% 9.87/3.41  cnf(ssp209, plain, (~spl28 | spl49 | spl128), inference(avatar_split_clause, [status(thm)], [p1346, sdef49, sdef128])).
% 9.87/3.41  cnf(p1348, plain, (apart_point_and_line(sk2,line_connecting(X0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(X0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_points(sk2,X0) | ~spl28), inference(resolution, [status(thm)], [p131, p975])).
% 9.87/3.41  cnf(ssp210, plain, (~spl28 | spl49 | spl109), inference(avatar_split_clause, [status(thm)], [p1348, sdef49, sdef109])).
% 9.87/3.41  cnf(p1349, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk1,sk2),X2) | distinct_lines(X0,X2) | ~spl17), inference(resolution, [status(thm)], [p131, p560])).
% 9.87/3.41  cnf(ssp211, plain, (~spl17 | spl49 | spl114), inference(avatar_split_clause, [status(thm)], [p1349, sdef49, sdef114])).
% 9.87/3.41  cnf(p1350, plain, (apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(sk2,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,sk2),X2) | distinct_lines(X2,X0) | ~spl17), inference(resolution, [status(thm)], [p131, p560])).
% 9.87/3.41  cnf(ssp212, plain, (~spl17 | spl51 | spl115), inference(avatar_split_clause, [status(thm)], [p1350, sdef51, sdef115])).
% 9.87/3.41  cnf(p1352, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk1,sk2)) | ~spl17), inference(resolution, [status(thm)], [p131, p979])).
% 9.87/3.41  cnf(ssp213, plain, (~spl17 | spl49 | spl116), inference(avatar_split_clause, [status(thm)], [p1352, sdef49, sdef116])).
% 9.87/3.41  cnf(p1353, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk1,sk0),X2) | distinct_lines(X0,X2) | ~spl18), inference(resolution, [status(thm)], [p131, p562])).
% 9.87/3.41  cnf(ssp214, plain, (~spl18 | spl49 | spl117), inference(avatar_split_clause, [status(thm)], [p1353, sdef49, sdef117])).
% 9.87/3.41  cnf(p1354, plain, (apart_point_and_line(sk2,line_connecting(sk1,sk0)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk1,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X2,X0) | ~spl18), inference(resolution, [status(thm)], [p131, p562])).
% 9.87/3.41  cnf(ssp215, plain, (~spl18 | spl52 | spl118), inference(avatar_split_clause, [status(thm)], [p1354, sdef52, sdef118])).
% 9.87/3.41  cnf(p1356, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk1,sk0)) | ~spl18), inference(resolution, [status(thm)], [p131, p984])).
% 9.87/3.41  cnf(ssp216, plain, (~spl18 | spl49 | spl119), inference(avatar_split_clause, [status(thm)], [p1356, sdef49, sdef119])).
% 9.87/3.41  cnf(p1357, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X0,X2) | ~spl19), inference(resolution, [status(thm)], [p131, p564])).
% 9.87/3.41  cnf(ssp217, plain, (~spl19 | spl54 | spl120), inference(avatar_split_clause, [status(thm)], [p1357, sdef54, sdef120])).
% 9.87/3.41  cnf(p1358, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,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),X2) | distinct_lines(X2,X0) | ~spl19), inference(resolution, [status(thm)], [p131, p564])).
% 9.87/3.41  cnf(ssp218, plain, (~spl19 | spl49 | spl121), inference(avatar_split_clause, [status(thm)], [p1358, sdef49, sdef121])).
% 9.87/3.41  cnf(p1360, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk0,sk2)) | ~spl19), inference(resolution, [status(thm)], [p131, p989])).
% 9.87/3.41  cnf(ssp219, plain, (~spl19 | spl54 | spl122), inference(avatar_split_clause, [status(thm)], [p1360, sdef54, sdef122])).
% 9.87/3.41  cnf(p1361, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk2,sk1),X2) | distinct_lines(X0,X2) | ~spl20), inference(resolution, [status(thm)], [p131, p566])).
% 9.87/3.41  cnf(ssp220, plain, (~spl20 | spl49 | spl123), inference(avatar_split_clause, [status(thm)], [p1361, sdef49, sdef123])).
% 9.87/3.41  cnf(p1362, plain, (apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,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,sk2),X2) | distinct_lines(X2,X0) | ~spl20), inference(resolution, [status(thm)], [p131, p566])).
% 9.87/3.41  cnf(ssp221, plain, (~spl20 | spl55 | spl124), inference(avatar_split_clause, [status(thm)], [p1362, sdef55, sdef124])).
% 9.87/3.41  cnf(p1364, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk2,sk1)) | ~spl20), inference(resolution, [status(thm)], [p131, p995])).
% 9.87/3.41  cnf(ssp222, plain, (~spl20 | spl49 | spl125), inference(avatar_split_clause, [status(thm)], [p1364, sdef49, sdef125])).
% 9.87/3.41  cnf(p1365, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(sk2,line_connecting(X0,X1)) | apart_point_and_line(X2,line_connecting(sk0,sk2)) | apart_point_and_line(X2,line_connecting(X0,X1)) | distinct_points(sk0,X2) | distinct_points(sk1,X0) | distinct_points(sk2,X1) | ~spl29), inference(resolution, [status(thm)], [p131, p568])).
% 9.87/3.41  fof(sdef134, definition, (spl134 <=> (apart_point_and_line(sk2,line_connecting(X0,X1)) | apart_point_and_line(X2,line_connecting(sk0,sk2)) | apart_point_and_line(X2,line_connecting(X0,X1)) | distinct_points(sk0,X2) | distinct_points(sk1,X0) | distinct_points(sk2,X1))), introduced(definition, [new_symbols(naming, [spl134])], [avatar_definition])).
% 9.87/3.41  cnf(ssp223, plain, (~spl29 | spl49 | spl134), inference(avatar_split_clause, [status(thm)], [p1365, sdef49, sdef134])).
% 9.87/3.41  cnf(sat_ref, plain, $false, inference(avatar_sat_refutation, [status(thm)], [ssp0, ssp1, ssp2, ssp3, ssp4, ssp5, ssp6, ssp7, ssp8, ssp9, ssp10, ssp11, ssp12, ssp13, ssp14, ssp15, ssp16, ssp17, ssp18, ssp19, ssp20, ssp21, ssp22, ssp23, ssp24, ssp25, ssp26, ssp27, ssp28, ssp29, ssp30, ssp31, ssp32, ssp33, ssp34, ssp35, ssp36, ssp37, ssp38, ssp39, ssp40, ssp41, ssp42, ssp43, ssp44, ssp45, ssp46, ssp47, ssp48, ssp49, ssp50, ssp51, ssp52, ssp53, ssp54, ssp55, ssp56, ssp57, ssp58, ssp59, ssp60, ssp61, ssp62, ssp63, ssp64, ssp65, ssp66, ssp67, ssp68, ssp69, ssp70, ssp71, ssp72, ssp73, ssp74, ssp75, ssp76, ssp77, ssp78, ssp79, ssp80, ssp81, ssp82, ssp83, ssp84, ssp85, ssp86, ssp87, ssp88, ssp89, ssp90, ssp91, ssp92, ssp93, ssp94, ssp95, ssp96, ssp97, ssp98, ssp99, ssp100, ssp101, ssp102, ssp103, ssp104, ssp105, ssp106, ssp107, ssp108, ssp109, ssp110, ssp111, ssp112, ssp113, ssp114, ssp115, ssp116, ssp117, ssp118, ssp119, ssp120, ssp121, ssp122, ssp123, ssp124, ssp125, ssp126, ssp127, ssp128, ssp129, ssp130, ssp131, ssp132, ssp133, ssp134, ssp135, ssp136, ssp137, ssp138, ssp139, ssp140, ssp141, ssp142, ssp143, ssp144, ssp145, ssp146, ssp147, ssp148, ssp149, ssp150, ssp151, ssp152, ssp153, ssp154, ssp155, ssp156, ssp157, ssp158, ssp159, ssp160, ssp161, ssp162, ssp163, ssp164, ssp165, ssp166, ssp167, ssp168, ssp169, ssp170, ssp171, ssp172, ssp173, ssp174, ssp175, ssp176, ssp177, ssp178, ssp179, ssp180, ssp181, ssp182, ssp183, ssp184, ssp185, ssp186, ssp187, ssp188, ssp189, ssp190, ssp191, ssp192, ssp193, ssp194, ssp195, ssp196, ssp197, ssp198, ssp199, ssp200, ssp201, ssp202, ssp203, ssp204, ssp205, ssp206, ssp207, ssp208, ssp209, ssp210, ssp211, ssp212, ssp213, ssp214, ssp215, ssp216, ssp217, ssp218, ssp219, ssp220, ssp221, ssp222, ssp223, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8, sct9, sct10, sct11, sct12])).
% 9.87/3.41  % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------