%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO173+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:17:15 PM UTC 2026
% Result : Theorem 18.81s 3.08s
% Output : Proof 18.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO173+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.57 % Computer : n006.cluster.edu
% 0.10/0.57 % Model : x86_64 x86_64
% 0.10/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.57 % Memory : 8046.5625MB
% 0.10/0.57 % OS : Linux 6.8.0-71-generic
% 0.10/0.57 % CPULimit : 300
% 0.10/0.57 % WCLimit : 300
% 0.10/0.57 % DateTime : Wed Sep 23 11:15:44 UTC 2026
% 0.10/0.57 % CPUTime :
% 0.10/0.57 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 18.81/3.08 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.81/3.08 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.81/3.08 fof(sdef0, definition, (spl0 <=> (apart_point_and_line(sk0,sk2))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 18.81/3.08 cnf(p919, plain, (apart_point_and_line(sk0,sk2) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 18.81/3.08 fof(f12, conjecture, ! [X,Y,U,V] : ( ( distinct_points(X,Y) & convergent_lines(U,V) & distinct_lines(U,line_connecting(X,Y)) ) => ( apart_point_and_line(X,U) | apart_point_and_line(Y,U) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 18.81/3.08 fof(f12_neg, negated_conjecture, ~(! [X,Y,U,V] : ( ( distinct_points(X,Y) & convergent_lines(U,V) & distinct_lines(U,line_connecting(X,Y)) ) => ( apart_point_and_line(X,U) | apart_point_and_line(Y,U) ) )), inference(negated_conjecture, [status(cth)], [f12])).
% 18.81/3.08 fof(f12_nnf, plain, ? [X,Y,U,V] : ((((distinct_points(X,Y) & convergent_lines(U,V)) & distinct_lines(U,line_connecting(X,Y))) & (~(apart_point_and_line(X,U)) & ~(apart_point_and_line(Y,U))))), inference(nnf_transformation, [status(thm)], [f12_neg])).
% 18.81/3.08 fof(f12_sk, plain, (((distinct_points(sk0,sk1) & convergent_lines(sk2,sk3)) & distinct_lines(sk2,line_connecting(sk0,sk1))) & (~(apart_point_and_line(sk0,sk2)) & ~(apart_point_and_line(sk1,sk2)))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2,sk3])], [f12_nnf])).
% 18.81/3.08 cnf(c17, plain, ~apart_point_and_line(sk0,sk2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 18.81/3.08 cnf(p1061, plain, ($false | ~spl0), inference(resolution, [status(thm)], [p919, c17])).
% 18.81/3.08 cnf(sct0, plain, (~spl0), inference(avatar_contradiction_clause, [status(thm)], [p1061])).
% 18.81/3.08 fof(sdef2, definition, (spl2 <=> (apart_point_and_line(sk1,sk2))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 18.81/3.08 cnf(p921, plain, (apart_point_and_line(sk1,sk2) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 18.81/3.08 cnf(c18, plain, ~apart_point_and_line(sk1,sk2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 18.81/3.08 cnf(p1062, plain, ($false | ~spl2), inference(resolution, [status(thm)], [p921, c18])).
% 18.81/3.08 cnf(sct1, plain, (~spl2), inference(avatar_contradiction_clause, [status(thm)], [p1062])).
% 18.81/3.08 fof(sdef1, definition, (spl1 <=> (apart_point_and_line(sk0,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 18.81/3.08 cnf(p920, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 18.81/3.08 fof(f6, axiom, ! [X,Y,Z] : ( distinct_points(X,Y) => ( apart_point_and_line(Z,line_connecting(X,Y)) => ( distinct_points(Z,X) & distinct_points(Z,Y) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con1)).
% 18.81/3.08 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])).
% 18.81/3.08 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])).
% 18.81/3.08 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])).
% 18.81/3.08 cnf(c14, plain, distinct_points(sk0,sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 18.81/3.08 cnf(p41, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c6, c14])).
% 18.81/3.08 cnf(p1223, plain, (distinct_points(sk0,sk0) | ~spl1), inference(resolution, [status(thm)], [p920, p41])).
% 18.81/3.08 fof(f0, axiom, ! [X] : ~ distinct_points(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart1)).
% 18.81/3.08 fof(f0_nnf, plain, ! [X] : (~(distinct_points(X,X))), inference(nnf_transformation, [status(thm)], [f0])).
% 18.81/3.08 fof(f0_sk, plain, ! [X] : (~(distinct_points(X,X))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 18.81/3.08 cnf(c0, plain, ~distinct_points(X0,X0), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 18.81/3.08 cnf(p1263, plain, ($false | ~spl1), inference(resolution, [status(thm)], [p1223, c0])).
% 18.81/3.08 cnf(sct2, plain, (~spl1), inference(avatar_contradiction_clause, [status(thm)], [p1263])).
% 18.81/3.08 fof(sdef3, definition, (spl3 <=> (apart_point_and_line(sk1,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 18.81/3.08 cnf(p922, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 18.81/3.08 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])).
% 18.81/3.08 cnf(p58, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [c7, c14])).
% 18.81/3.08 cnf(p1264, plain, (distinct_points(sk1,sk1) | ~spl3), inference(resolution, [status(thm)], [p922, p58])).
% 18.81/3.08 cnf(p1294, plain, ($false | ~spl3), inference(resolution, [status(thm)], [p1264, c0])).
% 18.81/3.08 cnf(sct3, plain, (~spl3), inference(avatar_contradiction_clause, [status(thm)], [p1294])).
% 18.81/3.08 fof(f8, axiom, ! [X,Y,U,V] : ( ( distinct_points(X,Y) & distinct_lines(U,V) ) => ( apart_point_and_line(X,U) | apart_point_and_line(X,V) | apart_point_and_line(Y,U) | apart_point_and_line(Y,V) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cu1)).
% 18.81/3.08 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])).
% 18.81/3.08 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])).
% 18.81/3.08 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])).
% 18.81/3.08 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])).
% 18.81/3.08 cnf(c16, plain, distinct_lines(sk2,line_connecting(sk0,sk1)), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 18.81/3.08 cnf(p918, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,line_connecting(sk0,sk1)), inference(resolution, [status(thm)], [p127, c16])).
% 18.81/3.08 cnf(ssp0, plain, (spl0 | spl1 | spl2 | spl3), inference(avatar_split_clause, [status(thm)], [p918, sdef0, sdef1, sdef2, sdef3])).
% 18.81/3.08 fof(f11, axiom, ! [X,Y] : ( convergent_lines(X,Y) => distinct_lines(X,Y) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ceq3)).
% 18.81/3.08 fof(f11_nnf, plain, ! [X,Y] : ((~(convergent_lines(X,Y)) | distinct_lines(X,Y))), inference(nnf_transformation, [status(thm)], [f11])).
% 18.81/3.08 fof(f11_sk, plain, ! [X,Y] : ((~(convergent_lines(X,Y)) | distinct_lines(X,Y))), inference(skolemisation, [status(esa)], [f11_nnf])).
% 18.81/3.08 cnf(c13, plain, ~convergent_lines(X0,X1) | distinct_lines(X0,X1), inference(cnf_transformation, [status(esa)], [f11_sk])).
% 18.81/3.08 cnf(c15, plain, convergent_lines(sk2,sk3), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 18.81/3.08 cnf(p19, plain, distinct_lines(sk2,sk3), inference(resolution, [status(thm)], [c13, c15])).
% 18.81/3.08 cnf(p923, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,sk3) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,sk3), inference(resolution, [status(thm)], [p127, p19])).
% 18.81/3.08 fof(sdef4, definition, (spl4 <=> (apart_point_and_line(sk0,sk3))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 18.81/3.08 fof(sdef5, definition, (spl5 <=> (apart_point_and_line(sk1,sk3))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 18.81/3.08 cnf(ssp1, plain, (spl0 | spl2 | spl4 | spl5), inference(avatar_split_clause, [status(thm)], [p923, sdef0, sdef2, sdef4, sdef5])).
% 18.81/3.08 fof(f4, axiom, ! [X,Y,Z] : ( distinct_lines(X,Y) => ( distinct_lines(X,Z) | distinct_lines(Y,Z) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart5)).
% 18.81/3.08 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])).
% 18.81/3.08 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])).
% 18.81/3.08 cnf(c4, plain, ~distinct_lines(X0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 18.81/3.08 cnf(p28, plain, distinct_lines(sk2,X0) | distinct_lines(sk3,X0), inference(resolution, [status(thm)], [c4, p19])).
% 18.81/3.08 cnf(p926, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [p127, p28])).
% 18.81/3.08 fof(sdef6, definition, (spl6 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 18.81/3.08 cnf(ssp2, plain, (spl4 | spl5 | spl6), inference(avatar_split_clause, [status(thm)], [p926, sdef4, sdef5, sdef6])).
% 18.81/3.08 cnf(p27, plain, distinct_lines(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X0), inference(resolution, [status(thm)], [c4, c16])).
% 18.81/3.08 cnf(p928, plain, apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [p127, p27])).
% 18.81/3.08 cnf(ssp3, plain, (spl1 | spl3 | spl6), inference(avatar_split_clause, [status(thm)], [p928, sdef1, sdef3, sdef6])).
% 18.81/3.08 cnf(p29, plain, distinct_lines(sk2,X0) | distinct_lines(sk3,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p28, c4])).
% 18.81/3.08 cnf(p929, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(sk3,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p127, p29])).
% 18.81/3.08 fof(sdef7, definition, (spl7 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(sk3,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 18.81/3.08 cnf(ssp4, plain, (spl0 | spl2 | spl7), inference(avatar_split_clause, [status(thm)], [p929, sdef0, sdef2, sdef7])).
% 18.81/3.08 cnf(p931, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p127, p29])).
% 18.81/3.08 fof(sdef8, definition, (spl8 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 18.81/3.08 cnf(ssp5, plain, (spl4 | spl5 | spl8), inference(avatar_split_clause, [status(thm)], [p931, sdef4, sdef5, sdef8])).
% 18.81/3.08 cnf(p933, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(sk2,X0) | distinct_lines(sk3,X1), inference(resolution, [status(thm)], [p127, p29])).
% 18.81/3.08 fof(sdef9, definition, (spl9 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(sk3,X0))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 18.81/3.08 cnf(ssp6, plain, (spl6 | spl9), inference(avatar_split_clause, [status(thm)], [p933, sdef6, sdef9])).
% 18.81/3.08 fof(f1, axiom, ! [X] : ~ distinct_lines(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart2)).
% 18.81/3.08 fof(f1_nnf, plain, ! [X] : (~(distinct_lines(X,X))), inference(nnf_transformation, [status(thm)], [f1])).
% 18.81/3.08 fof(f1_sk, plain, ! [X] : (~(distinct_lines(X,X))), inference(skolemisation, [status(esa)], [f1_nnf])).
% 18.81/3.08 cnf(c1, plain, ~distinct_lines(X0,X0), inference(cnf_transformation, [status(esa)], [f1_sk])).
% 18.81/3.08 cnf(p53, plain, distinct_lines(sk2,X0) | distinct_lines(X0,sk3), inference(resolution, [status(thm)], [p29, c1])).
% 18.81/3.08 cnf(p935, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(X0,sk3), inference(resolution, [status(thm)], [p127, p53])).
% 18.81/3.08 fof(sdef10, definition, (spl10 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X0,sk3))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 18.81/3.08 cnf(ssp7, plain, (spl0 | spl2 | spl10), inference(avatar_split_clause, [status(thm)], [p935, sdef0, sdef2, sdef10])).
% 18.81/3.08 fof(f5, axiom, ! [X,Y,Z] : ( convergent_lines(X,Y) => ( convergent_lines(X,Z) | convergent_lines(Y,Z) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart6)).
% 18.81/3.08 fof(f5_nnf, plain, ! [X,Y,Z] : ((~(convergent_lines(X,Y)) | (convergent_lines(X,Z) | convergent_lines(Y,Z)))), inference(nnf_transformation, [status(thm)], [f5])).
% 18.81/3.08 fof(f5_sk, plain, ! [X,Y,Z] : ((~(convergent_lines(X,Y)) | (convergent_lines(X,Z) | convergent_lines(Y,Z)))), inference(skolemisation, [status(esa)], [f5_nnf])).
% 18.81/3.08 cnf(c5, plain, ~convergent_lines(X0,X1) | convergent_lines(X0,X2) | convergent_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f5_sk])).
% 18.81/3.08 cnf(p36, plain, convergent_lines(sk2,X0) | convergent_lines(sk3,X0), inference(resolution, [status(thm)], [c5, c15])).
% 18.81/3.08 cnf(p37, plain, convergent_lines(sk2,X0) | distinct_lines(sk3,X0), inference(resolution, [status(thm)], [p36, c13])).
% 18.81/3.08 cnf(p40, plain, distinct_lines(sk3,X0) | convergent_lines(sk2,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p37, c5])).
% 18.81/3.08 fof(f2, axiom, ! [X] : ~ convergent_lines(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart3)).
% 18.81/3.08 fof(f2_nnf, plain, ! [X] : (~(convergent_lines(X,X))), inference(nnf_transformation, [status(thm)], [f2])).
% 18.81/3.08 fof(f2_sk, plain, ! [X] : (~(convergent_lines(X,X))), inference(skolemisation, [status(esa)], [f2_nnf])).
% 18.81/3.08 cnf(c2, plain, ~convergent_lines(X0,X0), inference(cnf_transformation, [status(esa)], [f2_sk])).
% 18.81/3.08 cnf(p115, plain, distinct_lines(sk3,X0) | convergent_lines(X0,sk2), inference(resolution, [status(thm)], [p40, c2])).
% 18.81/3.08 cnf(p124, plain, distinct_lines(sk3,X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p115, c13])).
% 18.81/3.08 cnf(p937, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p127, p124])).
% 18.81/3.08 fof(sdef11, definition, (spl11 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X0,sk2))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 18.81/3.08 cnf(ssp8, plain, (spl4 | spl5 | spl11), inference(avatar_split_clause, [status(thm)], [p937, sdef4, sdef5, sdef11])).
% 18.81/3.08 cnf(p939, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,sk2) | distinct_lines(sk3,X0), inference(resolution, [status(thm)], [p127, p124])).
% 18.81/3.08 cnf(ssp9, plain, (spl0 | spl2 | spl9), inference(avatar_split_clause, [status(thm)], [p939, sdef0, sdef2, sdef9])).
% 18.81/3.08 cnf(p57, plain, distinct_lines(X0,sk3) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p53, c4])).
% 18.81/3.08 cnf(p940, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,sk3) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p127, p57])).
% 18.81/3.08 fof(sdef12, definition, (spl12 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(sk2,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 18.81/3.08 cnf(ssp10, plain, (spl4 | spl5 | spl12), inference(avatar_split_clause, [status(thm)], [p940, sdef4, sdef5, sdef12])).
% 18.81/3.08 cnf(p942, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(X1,sk3) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p127, p57])).
% 18.81/3.08 fof(sdef13, definition, (spl13 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X1,sk3) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 18.81/3.08 cnf(ssp11, plain, (spl0 | spl2 | spl13), inference(avatar_split_clause, [status(thm)], [p942, sdef0, sdef2, sdef13])).
% 18.81/3.08 cnf(p944, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X0,sk3) | distinct_lines(sk2,X1), inference(resolution, [status(thm)], [p127, p57])).
% 18.81/3.08 cnf(ssp12, plain, (spl6 | spl10), inference(avatar_split_clause, [status(thm)], [p944, sdef6, sdef10])).
% 18.81/3.08 cnf(p38, plain, convergent_lines(sk2,X0) | convergent_lines(sk3,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p36, c5])).
% 18.81/3.08 cnf(p90, plain, convergent_lines(sk2,X0) | convergent_lines(sk3,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p38, c13])).
% 18.81/3.08 cnf(p945, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(sk2,X0) | convergent_lines(sk3,X1), inference(resolution, [status(thm)], [p127, p90])).
% 18.81/3.08 fof(sdef14, definition, (spl14 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 18.81/3.08 fof(sdef15, definition, (spl15 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk3,X0))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 18.81/3.08 cnf(ssp13, plain, (spl14 | spl15), inference(avatar_split_clause, [status(thm)], [p945, sdef14, sdef15])).
% 18.81/3.08 cnf(p117, plain, distinct_lines(sk3,X0) | convergent_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p40, c13])).
% 18.81/3.08 cnf(p948, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | convergent_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p127, p117])).
% 18.81/3.08 fof(sdef16, definition, (spl16 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk2,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 18.81/3.08 cnf(ssp14, plain, (spl4 | spl5 | spl16), inference(avatar_split_clause, [status(thm)], [p948, sdef4, sdef5, sdef16])).
% 18.81/3.08 cnf(p950, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(sk3,X0) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [p127, p117])).
% 18.81/3.08 cnf(ssp15, plain, (spl9 | spl14), inference(avatar_split_clause, [status(thm)], [p950, sdef9, sdef14])).
% 18.81/3.08 cnf(p140, plain, distinct_lines(X0,sk2) | distinct_lines(sk3,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p124, c4])).
% 18.81/3.08 cnf(p951, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p127, p140])).
% 18.81/3.08 fof(sdef17, definition, (spl17 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 18.81/3.08 cnf(ssp16, plain, (spl4 | spl5 | spl17), inference(avatar_split_clause, [status(thm)], [p951, sdef4, sdef5, sdef17])).
% 18.81/3.08 cnf(p953, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X0,sk2) | distinct_lines(sk3,X1), inference(resolution, [status(thm)], [p127, p140])).
% 18.81/3.08 cnf(ssp17, plain, (spl9 | spl11), inference(avatar_split_clause, [status(thm)], [p953, sdef9, sdef11])).
% 18.81/3.08 cnf(p141, plain, distinct_lines(sk3,X0) | distinct_lines(X0,X1) | distinct_lines(sk2,X1), inference(resolution, [status(thm)], [p124, c4])).
% 18.81/3.08 cnf(p954, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(sk3,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p127, p141])).
% 18.81/3.08 fof(sdef18, definition, (spl18 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(sk3,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 18.81/3.08 cnf(ssp18, plain, (spl0 | spl2 | spl18), inference(avatar_split_clause, [status(thm)], [p954, sdef0, sdef2, sdef18])).
% 18.81/3.08 cnf(p88, plain, convergent_lines(sk3,X0) | convergent_lines(X1,X0) | distinct_lines(sk2,X1), inference(resolution, [status(thm)], [p38, c13])).
% 18.81/3.08 cnf(p155, plain, convergent_lines(sk3,X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p88, c13])).
% 18.81/3.08 cnf(p956, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | convergent_lines(sk3,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p127, p155])).
% 18.81/3.08 fof(sdef19, definition, (spl19 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk3,X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 18.81/3.08 cnf(ssp19, plain, (spl0 | spl2 | spl19), inference(avatar_split_clause, [status(thm)], [p956, sdef0, sdef2, sdef19])).
% 18.81/3.08 cnf(p958, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(sk3,X1) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [p127, p155])).
% 18.81/3.08 cnf(ssp20, plain, (spl6 | spl15), inference(avatar_split_clause, [status(thm)], [p958, sdef6, sdef15])).
% 18.81/3.08 cnf(p89, plain, convergent_lines(sk2,X0) | convergent_lines(X0,X1) | distinct_lines(sk3,X1), inference(resolution, [status(thm)], [p38, c13])).
% 18.81/3.08 cnf(p164, plain, convergent_lines(sk2,X0) | distinct_lines(sk3,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p89, c13])).
% 18.81/3.08 cnf(p959, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | convergent_lines(sk2,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p127, p164])).
% 18.81/3.08 fof(sdef20, definition, (spl20 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk2,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 18.81/3.08 cnf(ssp21, plain, (spl4 | spl5 | spl20), inference(avatar_split_clause, [status(thm)], [p959, sdef4, sdef5, sdef20])).
% 18.81/3.08 cnf(p87, plain, convergent_lines(sk2,X0) | convergent_lines(X0,sk3), inference(resolution, [status(thm)], [p38, c2])).
% 18.81/3.08 cnf(p99, plain, convergent_lines(X0,sk3) | convergent_lines(sk2,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p87, c5])).
% 18.81/3.08 cnf(p179, plain, convergent_lines(X0,sk3) | convergent_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p99, c13])).
% 18.81/3.08 cnf(p961, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(X0,sk3) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [p127, p179])).
% 18.81/3.08 fof(sdef21, definition, (spl21 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(X0,sk3))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 18.81/3.08 cnf(ssp22, plain, (spl14 | spl21), inference(avatar_split_clause, [status(thm)], [p961, sdef14, sdef21])).
% 18.81/3.08 cnf(p30, plain, distinct_lines(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p27, c4])).
% 18.81/3.08 cnf(p963, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p127, p30])).
% 18.81/3.08 fof(sdef22, definition, (spl22 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 18.81/3.08 cnf(ssp23, plain, (spl0 | spl2 | spl22), inference(avatar_split_clause, [status(thm)], [p963, sdef0, sdef2, sdef22])).
% 18.81/3.08 cnf(p965, plain, apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p127, p30])).
% 18.81/3.08 cnf(ssp24, plain, (spl1 | spl3 | spl8), inference(avatar_split_clause, [status(thm)], [p965, sdef1, sdef3, sdef8])).
% 18.81/3.08 cnf(p966, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X1), inference(resolution, [status(thm)], [p127, p30])).
% 18.81/3.08 fof(sdef23, definition, (spl23 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 18.81/3.08 cnf(ssp25, plain, (spl6 | spl23), inference(avatar_split_clause, [status(thm)], [p966, sdef6, sdef23])).
% 18.81/3.08 cnf(p98, plain, convergent_lines(sk2,X0) | distinct_lines(X0,sk3), inference(resolution, [status(thm)], [p87, c13])).
% 18.81/3.08 cnf(p112, plain, distinct_lines(X0,sk3) | convergent_lines(sk2,X1) | convergent_lines(X0,X1), inference(resolution, [status(thm)], [p98, c5])).
% 18.81/3.08 cnf(p214, plain, distinct_lines(X0,sk3) | convergent_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p112, c13])).
% 18.81/3.08 cnf(p968, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X0,sk3) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [p127, p214])).
% 18.81/3.08 cnf(ssp26, plain, (spl10 | spl14), inference(avatar_split_clause, [status(thm)], [p968, sdef10, sdef14])).
% 18.81/3.08 cnf(p178, plain, convergent_lines(X0,sk3) | convergent_lines(X0,X1) | distinct_lines(sk2,X1), inference(resolution, [status(thm)], [p99, c13])).
% 18.81/3.08 cnf(p269, plain, convergent_lines(X0,sk3) | distinct_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p178, c13])).
% 18.81/3.08 cnf(p969, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | convergent_lines(X1,sk3) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p127, p269])).
% 18.81/3.08 fof(sdef24, definition, (spl24 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(X1,sk3) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 18.81/3.08 cnf(ssp27, plain, (spl0 | spl2 | spl24), inference(avatar_split_clause, [status(thm)], [p969, sdef0, sdef2, sdef24])).
% 18.81/3.08 cnf(p971, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(X0,sk3) | distinct_lines(sk2,X1), inference(resolution, [status(thm)], [p127, p269])).
% 18.81/3.08 cnf(ssp28, plain, (spl6 | spl21), inference(avatar_split_clause, [status(thm)], [p971, sdef6, sdef21])).
% 18.81/3.08 cnf(p177, plain, convergent_lines(X0,sk3) | convergent_lines(X0,sk2), inference(resolution, [status(thm)], [p99, c2])).
% 18.81/3.08 cnf(p190, plain, convergent_lines(X0,sk2) | convergent_lines(X0,X1) | convergent_lines(sk3,X1), inference(resolution, [status(thm)], [p177, c5])).
% 18.81/3.08 cnf(p292, plain, convergent_lines(X0,sk2) | convergent_lines(sk3,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p190, c13])).
% 18.81/3.08 cnf(p972, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(X0,sk2) | convergent_lines(sk3,X1), inference(resolution, [status(thm)], [p127, p292])).
% 18.81/3.08 fof(sdef25, definition, (spl25 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(X0,sk2))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 18.81/3.08 cnf(ssp29, plain, (spl15 | spl25), inference(avatar_split_clause, [status(thm)], [p972, sdef15, sdef25])).
% 18.81/3.08 cnf(p276, plain, convergent_lines(X0,sk3) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p179, c2])).
% 18.81/3.08 cnf(p288, plain, distinct_lines(X0,sk2) | convergent_lines(X0,X1) | convergent_lines(sk3,X1), inference(resolution, [status(thm)], [p276, c5])).
% 18.81/3.08 cnf(p357, plain, distinct_lines(X0,sk2) | convergent_lines(sk3,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p288, c13])).
% 18.81/3.08 cnf(p974, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X0,sk2) | convergent_lines(sk3,X1), inference(resolution, [status(thm)], [p127, p357])).
% 18.81/3.08 cnf(ssp30, plain, (spl11 | spl15), inference(avatar_split_clause, [status(thm)], [p974, sdef11, sdef15])).
% 18.81/3.08 cnf(p365, plain, convergent_lines(X0,sk2) | distinct_lines(X0,X1) | distinct_lines(sk3,X1), inference(resolution, [status(thm)], [p292, c13])).
% 18.81/3.08 cnf(p975, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(X0,sk2) | distinct_lines(sk3,X1), inference(resolution, [status(thm)], [p127, p365])).
% 18.81/3.08 cnf(ssp31, plain, (spl9 | spl25), inference(avatar_split_clause, [status(thm)], [p975, sdef9, sdef25])).
% 18.81/3.08 cnf(p976, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | convergent_lines(X1,sk2) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p127, p365])).
% 18.81/3.08 fof(sdef26, definition, (spl26 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(X1,sk2) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 18.81/3.08 cnf(ssp32, plain, (spl4 | spl5 | spl26), inference(avatar_split_clause, [status(thm)], [p976, sdef4, sdef5, sdef26])).
% 18.81/3.08 cnf(p291, plain, convergent_lines(X0,sk2) | convergent_lines(sk3,X0), inference(resolution, [status(thm)], [p190, c2])).
% 18.81/3.08 cnf(p303, plain, convergent_lines(sk3,X0) | convergent_lines(X0,X1) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [p291, c5])).
% 18.81/3.08 cnf(p377, plain, convergent_lines(sk3,X0) | convergent_lines(sk2,X1) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p303, c13])).
% 18.81/3.08 cnf(p407, plain, convergent_lines(sk3,X0) | distinct_lines(X0,X1) | distinct_lines(sk2,X1), inference(resolution, [status(thm)], [p377, c13])).
% 18.81/3.08 cnf(p978, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | convergent_lines(sk3,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p127, p407])).
% 18.81/3.08 fof(sdef27, definition, (spl27 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk3,X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 18.81/3.08 cnf(ssp33, plain, (spl0 | spl2 | spl27), inference(avatar_split_clause, [status(thm)], [p978, sdef0, sdef2, sdef27])).
% 18.81/3.08 cnf(p54, plain, distinct_lines(sk3,X0) | distinct_lines(X1,X0) | distinct_lines(sk2,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p29, c4])).
% 18.81/3.08 cnf(p980, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(sk2,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p127, p54])).
% 18.81/3.08 fof(sdef28, definition, (spl28 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X1,X0) | distinct_lines(sk2,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 18.81/3.08 cnf(ssp34, plain, (spl4 | spl5 | spl28), inference(avatar_split_clause, [status(thm)], [p980, sdef4, sdef5, sdef28])).
% 18.81/3.08 cnf(p982, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(sk3,X1) | distinct_lines(sk2,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p127, p54])).
% 18.81/3.08 cnf(ssp35, plain, (spl9 | spl12), inference(avatar_split_clause, [status(thm)], [p982, sdef9, sdef12])).
% 18.81/3.08 cnf(p983, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(sk3,X1) | distinct_lines(X2,X1) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p127, p54])).
% 18.81/3.08 fof(sdef29, definition, (spl29 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(sk3,X1) | distinct_lines(X2,X1) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 18.81/3.08 cnf(ssp36, plain, (spl0 | spl2 | spl29), inference(avatar_split_clause, [status(thm)], [p983, sdef0, sdef2, sdef29])).
% 18.81/3.08 cnf(p985, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(sk3,X2) | distinct_lines(X0,X2) | distinct_lines(sk2,X1), inference(resolution, [status(thm)], [p127, p54])).
% 18.81/3.08 cnf(ssp37, plain, (spl6 | spl7), inference(avatar_split_clause, [status(thm)], [p985, sdef6, sdef7])).
% 18.81/3.08 cnf(p55, plain, distinct_lines(sk2,X0) | distinct_lines(X0,X1) | distinct_lines(sk3,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p29, c4])).
% 18.81/3.08 cnf(p986, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(sk3,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p127, p55])).
% 18.81/3.08 fof(sdef30, definition, (spl30 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(sk3,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 18.81/3.08 cnf(ssp38, plain, (spl0 | spl2 | spl30), inference(avatar_split_clause, [status(thm)], [p986, sdef0, sdef2, sdef30])).
% 18.81/3.08 cnf(p988, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p127, p55])).
% 18.81/3.08 fof(sdef31, definition, (spl31 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 18.81/3.08 cnf(ssp39, plain, (spl4 | spl5 | spl31), inference(avatar_split_clause, [status(thm)], [p988, sdef4, sdef5, sdef31])).
% 18.81/3.08 cnf(p990, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(sk2,X2) | distinct_lines(X2,X0) | distinct_lines(sk3,X1), inference(resolution, [status(thm)], [p127, p55])).
% 18.81/3.08 cnf(ssp40, plain, (spl8 | spl9), inference(avatar_split_clause, [status(thm)], [p990, sdef8, sdef9])).
% 18.81/3.08 cnf(p428, plain, distinct_lines(sk2,X0) | distinct_lines(X0,X1) | distinct_lines(X1,sk3), inference(resolution, [status(thm)], [p55, c1])).
% 18.81/3.08 cnf(p991, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(X1,sk3), inference(resolution, [status(thm)], [p127, p428])).
% 18.81/3.08 fof(sdef32, definition, (spl32 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(X1,sk3))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 18.81/3.08 cnf(ssp41, plain, (spl0 | spl2 | spl32), inference(avatar_split_clause, [status(thm)], [p991, sdef0, sdef2, sdef32])).
% 18.81/3.08 cnf(p56, plain, distinct_lines(sk2,X0) | distinct_lines(sk3,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p29, c4])).
% 18.81/3.08 cnf(p993, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(sk3,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p127, p56])).
% 18.81/3.08 fof(sdef33, definition, (spl33 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(sk3,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 18.81/3.08 cnf(ssp42, plain, (spl0 | spl2 | spl33), inference(avatar_split_clause, [status(thm)], [p993, sdef0, sdef2, sdef33])).
% 18.81/3.08 cnf(p995, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p127, p56])).
% 18.81/3.08 fof(sdef34, definition, (spl34 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 18.81/3.08 cnf(ssp43, plain, (spl4 | spl5 | spl34), inference(avatar_split_clause, [status(thm)], [p995, sdef4, sdef5, sdef34])).
% 18.81/3.08 cnf(p997, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(sk2,X0) | distinct_lines(sk3,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p127, p56])).
% 18.81/3.08 cnf(ssp44, plain, (spl6 | spl18), inference(avatar_split_clause, [status(thm)], [p997, sdef6, sdef18])).
% 18.81/3.08 cnf(p92, plain, convergent_lines(sk2,X0) | convergent_lines(X0,X1) | convergent_lines(sk3,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p38, c5])).
% 18.81/3.08 cnf(p490, plain, convergent_lines(sk2,X0) | convergent_lines(X0,X1) | convergent_lines(X1,sk3), inference(resolution, [status(thm)], [p92, c2])).
% 18.81/3.08 cnf(p503, plain, convergent_lines(X0,X1) | convergent_lines(X1,sk3) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [p490, c13])).
% 18.81/3.08 cnf(p513, plain, convergent_lines(X0,sk3) | distinct_lines(sk2,X1) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p503, c13])).
% 18.81/3.08 cnf(p998, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | convergent_lines(X1,sk3) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p127, p513])).
% 18.81/3.08 fof(sdef35, definition, (spl35 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(X1,sk3) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 18.81/3.08 cnf(ssp45, plain, (spl0 | spl2 | spl35), inference(avatar_split_clause, [status(thm)], [p998, sdef0, sdef2, sdef35])).
% 18.81/3.08 cnf(p118, plain, distinct_lines(sk3,X0) | convergent_lines(X0,X1) | convergent_lines(sk2,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p40, c5])).
% 18.81/3.08 cnf(p549, plain, distinct_lines(sk3,X0) | convergent_lines(X0,X1) | convergent_lines(X1,sk2), inference(resolution, [status(thm)], [p118, c2])).
% 18.81/3.08 cnf(p561, plain, distinct_lines(sk3,X0) | convergent_lines(X1,sk2) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p549, c13])).
% 18.81/3.08 cnf(p1000, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | convergent_lines(X1,sk2) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p127, p561])).
% 18.81/3.08 fof(sdef36, definition, (spl36 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(X1,sk2) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 18.81/3.08 cnf(ssp46, plain, (spl4 | spl5 | spl36), inference(avatar_split_clause, [status(thm)], [p1000, sdef4, sdef5, sdef36])).
% 18.81/3.08 cnf(p567, plain, distinct_lines(sk3,X0) | distinct_lines(X0,X1) | distinct_lines(X1,sk2), inference(resolution, [status(thm)], [p561, c13])).
% 18.81/3.08 cnf(p1002, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(X1,sk2), inference(resolution, [status(thm)], [p127, p567])).
% 18.81/3.08 fof(sdef37, definition, (spl37 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(X1,sk2))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 18.81/3.08 cnf(ssp47, plain, (spl4 | spl5 | spl37), inference(avatar_split_clause, [status(thm)], [p1002, sdef4, sdef5, sdef37])).
% 18.81/3.08 cnf(p143, plain, distinct_lines(X0,sk3) | distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p57, c4])).
% 18.81/3.08 cnf(p1004, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,sk3) | distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p127, p143])).
% 18.81/3.08 fof(sdef38, definition, (spl38 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 18.81/3.08 cnf(ssp48, plain, (spl4 | spl5 | spl38), inference(avatar_split_clause, [status(thm)], [p1004, sdef4, sdef5, sdef38])).
% 18.81/3.08 cnf(p1006, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X0,sk3) | distinct_lines(sk2,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p127, p143])).
% 18.81/3.08 cnf(ssp49, plain, (spl10 | spl12), inference(avatar_split_clause, [status(thm)], [p1006, sdef10, sdef12])).
% 18.81/3.08 cnf(p1007, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(X1,sk3) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p127, p143])).
% 18.81/3.08 fof(sdef39, definition, (spl39 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X1,sk3) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 18.81/3.08 cnf(ssp50, plain, (spl0 | spl2 | spl39), inference(avatar_split_clause, [status(thm)], [p1007, sdef0, sdef2, sdef39])).
% 18.81/3.08 cnf(p1009, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X2,sk3) | distinct_lines(X2,X0) | distinct_lines(sk2,X1), inference(resolution, [status(thm)], [p127, p143])).
% 18.81/3.08 cnf(ssp51, plain, (spl6 | spl13), inference(avatar_split_clause, [status(thm)], [p1009, sdef6, sdef13])).
% 18.81/3.08 cnf(p583, plain, distinct_lines(X0,sk3) | distinct_lines(X0,X1) | distinct_lines(X1,sk2), inference(resolution, [status(thm)], [p143, c1])).
% 18.81/3.08 cnf(p1010, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X0,sk3) | distinct_lines(X1,sk2), inference(resolution, [status(thm)], [p127, p583])).
% 18.81/3.08 cnf(ssp52, plain, (spl10 | spl11), inference(avatar_split_clause, [status(thm)], [p1010, sdef10, sdef11])).
% 18.81/3.08 cnf(p144, plain, distinct_lines(X0,sk3) | distinct_lines(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p57, c4])).
% 18.81/3.08 cnf(p1011, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(X1,sk3) | distinct_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p127, p144])).
% 18.81/3.08 fof(sdef40, definition, (spl40 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X1,sk3) | distinct_lines(X1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 18.81/3.08 cnf(ssp53, plain, (spl0 | spl2 | spl40), inference(avatar_split_clause, [status(thm)], [p1011, sdef0, sdef2, sdef40])).
% 18.81/3.08 cnf(p1013, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X0,sk3) | distinct_lines(sk2,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p127, p144])).
% 18.81/3.08 cnf(ssp54, plain, (spl8 | spl10), inference(avatar_split_clause, [status(thm)], [p1013, sdef8, sdef10])).
% 18.81/3.08 cnf(p170, plain, convergent_lines(sk2,X0) | convergent_lines(sk3,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p90, c4])).
% 18.81/3.08 cnf(p1014, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(sk2,X0) | convergent_lines(sk3,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p127, p170])).
% 18.81/3.08 cnf(ssp55, plain, (spl14 | spl27), inference(avatar_split_clause, [status(thm)], [p1014, sdef14, sdef27])).
% 18.81/3.08 cnf(p1015, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(sk2,X2) | convergent_lines(sk3,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p127, p170])).
% 18.81/3.08 cnf(ssp56, plain, (spl15 | spl20), inference(avatar_split_clause, [status(thm)], [p1015, sdef15, sdef20])).
% 18.81/3.08 cnf(p171, plain, convergent_lines(sk3,X0) | distinct_lines(X1,X0) | convergent_lines(sk2,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p90, c5])).
% 18.81/3.08 cnf(p1016, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(sk3,X1) | convergent_lines(sk2,X2) | convergent_lines(X0,X2), inference(resolution, [status(thm)], [p127, p171])).
% 18.81/3.08 fof(sdef41, definition, (spl41 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk2,X1) | convergent_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 18.81/3.08 cnf(ssp57, plain, (spl15 | spl41), inference(avatar_split_clause, [status(thm)], [p1016, sdef15, sdef41])).
% 18.81/3.08 cnf(p172, plain, convergent_lines(sk2,X0) | distinct_lines(X0,X1) | convergent_lines(sk3,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p90, c5])).
% 18.81/3.08 cnf(p1018, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(sk2,X0) | convergent_lines(sk3,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p127, p172])).
% 18.81/3.08 fof(sdef42, definition, (spl42 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk3,X1) | convergent_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 18.81/3.08 cnf(ssp58, plain, (spl14 | spl42), inference(avatar_split_clause, [status(thm)], [p1018, sdef14, sdef42])).
% 18.81/3.08 cnf(p180, plain, convergent_lines(X0,sk3) | convergent_lines(X0,X1) | convergent_lines(sk2,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p99, c5])).
% 18.81/3.08 cnf(p660, plain, convergent_lines(X0,sk3) | convergent_lines(X0,X1) | convergent_lines(X1,sk2), inference(resolution, [status(thm)], [p180, c2])).
% 18.81/3.09 cnf(p675, plain, convergent_lines(X0,sk3) | convergent_lines(X1,sk2) | distinct_lines(X0,X1), inference(resolution, [status(thm)], [p660, c13])).
% 18.81/3.09 cnf(p1020, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(X0,sk3) | convergent_lines(X1,sk2), inference(resolution, [status(thm)], [p127, p675])).
% 18.81/3.09 cnf(ssp59, plain, (spl21 | spl25), inference(avatar_split_clause, [status(thm)], [p1020, sdef21, sdef25])).
% 18.81/3.09 cnf(p674, plain, convergent_lines(X0,X1) | convergent_lines(X1,sk2) | distinct_lines(X0,sk3), inference(resolution, [status(thm)], [p660, c13])).
% 18.81/3.09 cnf(p685, plain, convergent_lines(X0,sk2) | distinct_lines(X1,sk3) | distinct_lines(X1,X0), inference(resolution, [status(thm)], [p674, c13])).
% 18.81/3.09 cnf(p1021, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(X1,sk2) | distinct_lines(X0,sk3), inference(resolution, [status(thm)], [p127, p685])).
% 18.81/3.09 cnf(ssp60, plain, (spl10 | spl25), inference(avatar_split_clause, [status(thm)], [p1021, sdef10, sdef25])).
% 18.81/3.09 cnf(p692, plain, convergent_lines(X0,sk3) | distinct_lines(X0,X1) | distinct_lines(X1,sk2), inference(resolution, [status(thm)], [p675, c13])).
% 18.81/3.09 cnf(p1022, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(X0,sk3) | distinct_lines(X1,sk2), inference(resolution, [status(thm)], [p127, p692])).
% 18.81/3.09 cnf(ssp61, plain, (spl11 | spl21), inference(avatar_split_clause, [status(thm)], [p1022, sdef11, sdef21])).
% 18.81/3.09 cnf(p238, plain, convergent_lines(sk2,X0) | distinct_lines(X1,X0) | distinct_lines(sk3,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p117, c4])).
% 18.81/3.09 cnf(p1023, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(sk2,X1) | distinct_lines(sk3,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p127, p238])).
% 18.81/3.09 cnf(ssp62, plain, (spl7 | spl14), inference(avatar_split_clause, [status(thm)], [p1023, sdef7, sdef14])).
% 18.81/3.09 cnf(p1024, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | convergent_lines(sk2,X1) | distinct_lines(X2,X1) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p127, p238])).
% 18.81/3.09 fof(sdef43, definition, (spl43 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk2,X1) | distinct_lines(X2,X1) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 18.81/3.09 cnf(ssp63, plain, (spl4 | spl5 | spl43), inference(avatar_split_clause, [status(thm)], [p1024, sdef4, sdef5, sdef43])).
% 18.81/3.09 cnf(p1026, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(sk2,X2) | distinct_lines(X0,X2) | distinct_lines(sk3,X1), inference(resolution, [status(thm)], [p127, p238])).
% 18.81/3.09 cnf(ssp64, plain, (spl9 | spl16), inference(avatar_split_clause, [status(thm)], [p1026, sdef9, sdef16])).
% 18.81/3.09 cnf(p239, plain, distinct_lines(sk3,X0) | convergent_lines(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p117, c4])).
% 18.81/3.09 cnf(p1027, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | convergent_lines(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p127, p239])).
% 18.81/3.09 fof(sdef44, definition, (spl44 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 18.81/3.09 cnf(ssp65, plain, (spl4 | spl5 | spl44), inference(avatar_split_clause, [status(thm)], [p1027, sdef4, sdef5, sdef44])).
% 18.81/3.09 cnf(p1029, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(sk3,X0) | convergent_lines(sk2,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p127, p239])).
% 18.81/3.09 cnf(ssp66, plain, (spl9 | spl20), inference(avatar_split_clause, [status(thm)], [p1029, sdef9, sdef20])).
% 18.81/3.09 cnf(p1030, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(sk3,X2) | convergent_lines(sk2,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p127, p239])).
% 18.81/3.09 cnf(ssp67, plain, (spl14 | spl18), inference(avatar_split_clause, [status(thm)], [p1030, sdef14, sdef18])).
% 18.81/3.09 cnf(p240, plain, distinct_lines(sk3,X0) | distinct_lines(X0,X1) | convergent_lines(sk2,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p117, c5])).
% 18.81/3.09 cnf(p1031, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | distinct_lines(X0,X1) | convergent_lines(sk2,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p127, p240])).
% 18.81/3.09 fof(sdef45, definition, (spl45 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X0,X1) | convergent_lines(sk2,X2) | convergent_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 18.81/3.09 cnf(ssp68, plain, (spl4 | spl5 | spl45), inference(avatar_split_clause, [status(thm)], [p1031, sdef4, sdef5, sdef45])).
% 18.81/3.09 cnf(p1033, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(sk3,X0) | convergent_lines(sk2,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p127, p240])).
% 18.81/3.09 cnf(ssp69, plain, (spl9 | spl41), inference(avatar_split_clause, [status(thm)], [p1033, sdef9, sdef41])).
% 18.81/3.09 cnf(p243, plain, distinct_lines(X0,sk2) | distinct_lines(X0,X1) | distinct_lines(sk3,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p140, c4])).
% 18.81/3.09 cnf(p1034, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X0,sk2) | distinct_lines(sk3,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p127, p243])).
% 18.81/3.09 cnf(ssp70, plain, (spl7 | spl11), inference(avatar_split_clause, [status(thm)], [p1034, sdef7, sdef11])).
% 18.81/3.09 cnf(p1035, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p127, p243])).
% 18.81/3.09 fof(sdef46, definition, (spl46 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 18.81/3.09 cnf(ssp71, plain, (spl4 | spl5 | spl46), inference(avatar_split_clause, [status(thm)], [p1035, sdef4, sdef5, sdef46])).
% 18.81/3.09 cnf(p1037, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X2,sk2) | distinct_lines(X2,X0) | distinct_lines(sk3,X1), inference(resolution, [status(thm)], [p127, p243])).
% 18.81/3.09 cnf(ssp72, plain, (spl9 | spl17), inference(avatar_split_clause, [status(thm)], [p1037, sdef9, sdef17])).
% 18.81/3.09 cnf(p244, plain, distinct_lines(X0,sk2) | distinct_lines(sk3,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p140, c4])).
% 18.81/3.09 cnf(p1038, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p127, p244])).
% 18.81/3.09 fof(sdef47, definition, (spl47 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X1,sk2) | distinct_lines(X1,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 18.81/3.09 cnf(ssp73, plain, (spl4 | spl5 | spl47), inference(avatar_split_clause, [status(thm)], [p1038, sdef4, sdef5, sdef47])).
% 18.81/3.09 cnf(p1040, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X0,sk2) | distinct_lines(sk3,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p127, p244])).
% 18.81/3.09 cnf(ssp74, plain, (spl11 | spl18), inference(avatar_split_clause, [status(thm)], [p1040, sdef11, sdef18])).
% 18.81/3.09 cnf(p245, plain, distinct_lines(sk3,X0) | distinct_lines(X0,X1) | distinct_lines(sk2,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p141, c4])).
% 18.81/3.09 cnf(p1041, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(sk3,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p127, p245])).
% 18.81/3.09 fof(sdef48, definition, (spl48 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(sk3,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 18.81/3.09 cnf(ssp75, plain, (spl0 | spl2 | spl48), inference(avatar_split_clause, [status(thm)], [p1041, sdef0, sdef2, sdef48])).
% 18.81/3.09 cnf(p260, plain, convergent_lines(sk3,X0) | distinct_lines(X1,X0) | distinct_lines(sk2,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p155, c4])).
% 18.81/3.09 cnf(p1043, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(sk3,X1) | distinct_lines(sk2,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p127, p260])).
% 18.81/3.09 cnf(ssp76, plain, (spl12 | spl15), inference(avatar_split_clause, [status(thm)], [p1043, sdef12, sdef15])).
% 18.81/3.09 cnf(p1044, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | convergent_lines(sk3,X1) | distinct_lines(X2,X1) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p127, p260])).
% 18.81/3.09 fof(sdef49, definition, (spl49 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk3,X1) | distinct_lines(X2,X1) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 18.81/3.09 cnf(ssp77, plain, (spl0 | spl2 | spl49), inference(avatar_split_clause, [status(thm)], [p1044, sdef0, sdef2, sdef49])).
% 18.81/3.09 cnf(p1046, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(sk3,X2) | distinct_lines(X0,X2) | distinct_lines(sk2,X1), inference(resolution, [status(thm)], [p127, p260])).
% 18.81/3.09 cnf(ssp78, plain, (spl6 | spl19), inference(avatar_split_clause, [status(thm)], [p1046, sdef6, sdef19])).
% 18.81/3.09 cnf(p261, plain, convergent_lines(sk3,X0) | distinct_lines(sk2,X1) | distinct_lines(X1,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p155, c4])).
% 18.81/3.09 cnf(p1047, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | convergent_lines(sk3,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p127, p261])).
% 18.81/3.09 fof(sdef50, definition, (spl50 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk3,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 18.81/3.09 cnf(ssp79, plain, (spl0 | spl2 | spl50), inference(avatar_split_clause, [status(thm)], [p1047, sdef0, sdef2, sdef50])).
% 18.81/3.09 cnf(p1049, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(sk3,X2) | distinct_lines(sk2,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p127, p261])).
% 18.81/3.09 cnf(ssp80, plain, (spl6 | spl27), inference(avatar_split_clause, [status(thm)], [p1049, sdef6, sdef27])).
% 18.81/3.09 cnf(p1050, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(sk3,X0) | distinct_lines(sk2,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p127, p261])).
% 18.81/3.09 cnf(ssp81, plain, (spl8 | spl15), inference(avatar_split_clause, [status(thm)], [p1050, sdef8, sdef15])).
% 18.81/3.09 cnf(p262, plain, distinct_lines(sk2,X0) | distinct_lines(X0,X1) | convergent_lines(sk3,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p155, c5])).
% 18.81/3.09 cnf(p1051, plain, apart_point_and_line(sk0,sk2) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | distinct_lines(X0,X1) | convergent_lines(sk3,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p127, p262])).
% 18.81/3.09 fof(sdef51, definition, (spl51 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X0,X1) | convergent_lines(sk3,X2) | convergent_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 18.81/3.09 cnf(ssp82, plain, (spl0 | spl2 | spl51), inference(avatar_split_clause, [status(thm)], [p1051, sdef0, sdef2, sdef51])).
% 18.81/3.09 cnf(p1053, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(sk2,X0) | convergent_lines(sk3,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p127, p262])).
% 18.81/3.09 cnf(ssp83, plain, (spl6 | spl42), inference(avatar_split_clause, [status(thm)], [p1053, sdef6, sdef42])).
% 18.81/3.09 cnf(p265, plain, convergent_lines(sk2,X0) | distinct_lines(X0,X1) | distinct_lines(sk3,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p164, c4])).
% 18.81/3.09 cnf(p1054, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | convergent_lines(sk2,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p127, p265])).
% 18.81/3.09 fof(sdef52, definition, (spl52 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | convergent_lines(sk2,X1) | distinct_lines(X1,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 18.81/3.09 cnf(ssp84, plain, (spl4 | spl5 | spl52), inference(avatar_split_clause, [status(thm)], [p1054, sdef4, sdef5, sdef52])).
% 18.81/3.09 cnf(p266, plain, distinct_lines(sk3,X0) | distinct_lines(X1,X0) | convergent_lines(sk2,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p164, c5])).
% 18.81/3.09 cnf(p1056, plain, apart_point_and_line(sk0,sk3) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | distinct_lines(X1,X0) | convergent_lines(sk2,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p127, p266])).
% 18.81/3.09 fof(sdef53, definition, (spl53 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X1,X0) | convergent_lines(sk2,X2) | convergent_lines(X1,X2))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 18.81/3.09 cnf(ssp85, plain, (spl4 | spl5 | spl53), inference(avatar_split_clause, [status(thm)], [p1056, sdef4, sdef5, sdef53])).
% 18.81/3.09 cnf(p277, plain, convergent_lines(X0,sk3) | convergent_lines(sk2,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(resolution, [status(thm)], [p179, c4])).
% 18.81/3.09 cnf(p1058, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(X0,sk3) | convergent_lines(sk2,X2) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p127, p277])).
% 18.81/3.09 cnf(ssp86, plain, (spl20 | spl21), inference(avatar_split_clause, [status(thm)], [p1058, sdef20, sdef21])).
% 18.81/3.09 cnf(p1059, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(X2,sk3) | convergent_lines(sk2,X0) | distinct_lines(X2,X1), inference(resolution, [status(thm)], [p127, p277])).
% 18.81/3.09 cnf(ssp87, plain, (spl14 | spl24), inference(avatar_split_clause, [status(thm)], [p1059, sdef14, sdef24])).
% 18.81/3.09 cnf(p279, plain, convergent_lines(X0,sk3) | distinct_lines(X0,X1) | convergent_lines(sk2,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p179, c5])).
% 18.81/3.09 cnf(p1060, plain, apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | convergent_lines(X0,sk3) | convergent_lines(sk2,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [p127, p279])).
% 18.81/3.09 cnf(ssp88, plain, (spl21 | spl41), inference(avatar_split_clause, [status(thm)], [p1060, sdef21, sdef41])).
% 18.81/3.09 fof(f3, axiom, ! [X,Y,Z] : ( distinct_points(X,Y) => ( distinct_points(X,Z) | distinct_points(Y,Z) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart4)).
% 18.81/3.09 fof(f3_nnf, plain, ! [X,Y,Z] : ((~(distinct_points(X,Y)) | (distinct_points(X,Z) | distinct_points(Y,Z)))), inference(nnf_transformation, [status(thm)], [f3])).
% 18.81/3.09 fof(f3_sk, plain, ! [X,Y,Z] : ((~(distinct_points(X,Y)) | (distinct_points(X,Z) | distinct_points(Y,Z)))), inference(skolemisation, [status(esa)], [f3_nnf])).
% 18.81/3.09 cnf(c3, plain, ~distinct_points(X0,X1) | distinct_points(X0,X2) | distinct_points(X1,X2), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 18.81/3.09 cnf(p20, plain, distinct_points(sk0,X0) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [c3, c14])).
% 18.81/3.09 cnf(p128, 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, p20])).
% 18.81/3.09 cnf(p1089, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(X0,sk2) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p128, c16])).
% 18.81/3.09 fof(sdef54, definition, (spl54 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 18.81/3.09 cnf(ssp89, plain, (spl2 | spl3 | spl54), inference(avatar_split_clause, [status(thm)], [p1089, sdef2, sdef3, sdef54])).
% 18.81/3.09 cnf(p1091, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,sk3) | apart_point_and_line(X0,sk2) | apart_point_and_line(X0,sk3) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [p128, p19])).
% 18.81/3.09 fof(sdef55, definition, (spl55 <=> (apart_point_and_line(X0,sk2) | apart_point_and_line(X0,sk3) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 18.81/3.09 cnf(ssp90, plain, (spl2 | spl5 | spl55), inference(avatar_split_clause, [status(thm)], [p1091, sdef2, sdef5, sdef55])).
% 18.81/3.09 cnf(p1093, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [p128, p28])).
% 18.81/3.09 fof(sdef56, definition, (spl56 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 18.81/3.09 cnf(ssp91, plain, (spl5 | spl56), inference(avatar_split_clause, [status(thm)], [p1093, sdef5, sdef56])).
% 18.81/3.09 cnf(p1095, plain, apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk2,X0), inference(resolution, [status(thm)], [p128, p27])).
% 18.81/3.09 fof(sdef57, definition, (spl57 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 18.81/3.09 cnf(ssp92, plain, (spl3 | spl57), inference(avatar_split_clause, [status(thm)], [p1095, sdef3, sdef57])).
% 18.81/3.09 cnf(p1097, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk3,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p128, p29])).
% 18.81/3.09 fof(sdef58, definition, (spl58 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk3,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 18.81/3.09 cnf(ssp93, plain, (spl2 | spl58), inference(avatar_split_clause, [status(thm)], [p1097, sdef2, sdef58])).
% 18.81/3.09 cnf(p1099, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk2,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p128, p29])).
% 18.81/3.09 fof(sdef59, definition, (spl59 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk2,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 18.81/3.09 cnf(ssp94, plain, (spl5 | spl59), inference(avatar_split_clause, [status(thm)], [p1099, sdef5, sdef59])).
% 18.81/3.09 cnf(p1102, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,sk3), inference(resolution, [status(thm)], [p128, p53])).
% 18.81/3.09 fof(sdef60, definition, (spl60 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,sk3))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 18.81/3.09 cnf(ssp95, plain, (spl2 | spl60), inference(avatar_split_clause, [status(thm)], [p1102, sdef2, sdef60])).
% 18.81/3.09 cnf(p1104, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p128, p124])).
% 18.81/3.09 fof(sdef61, definition, (spl61 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,sk2))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 18.81/3.09 cnf(ssp96, plain, (spl5 | spl61), inference(avatar_split_clause, [status(thm)], [p1104, sdef5, sdef61])).
% 18.81/3.09 cnf(p1106, plain, apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,sk2) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk2) | distinct_points(sk0,X1) | distinct_lines(sk3,X0), inference(resolution, [status(thm)], [p128, p124])).
% 18.81/3.09 fof(sdef62, definition, (spl62 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk2) | distinct_points(sk0,X1) | distinct_lines(sk3,X0))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 18.81/3.09 cnf(ssp97, plain, (spl2 | spl62), inference(avatar_split_clause, [status(thm)], [p1106, sdef2, sdef62])).
% 18.81/3.09 cnf(p1108, plain, apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk3) | distinct_points(sk0,X1) | distinct_lines(sk2,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p128, p57])).
% 18.81/3.09 fof(sdef63, definition, (spl63 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk3) | distinct_points(sk0,X1) | distinct_lines(sk2,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 18.81/3.09 cnf(ssp98, plain, (spl5 | spl63), inference(avatar_split_clause, [status(thm)], [p1108, sdef5, sdef63])).
% 18.81/3.09 cnf(p1110, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,sk3) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p128, p57])).
% 18.81/3.09 fof(sdef64, definition, (spl64 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,sk3) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 18.81/3.09 cnf(ssp99, plain, (spl2 | spl64), inference(avatar_split_clause, [status(thm)], [p1110, sdef2, sdef64])).
% 18.81/3.09 cnf(p1114, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk2,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p128, p117])).
% 18.81/3.09 fof(sdef65, definition, (spl65 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk2,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 18.81/3.09 cnf(ssp100, plain, (spl5 | spl65), inference(avatar_split_clause, [status(thm)], [p1114, sdef5, sdef65])).
% 18.81/3.09 cnf(p1117, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,sk2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p128, p140])).
% 18.81/3.09 fof(sdef66, definition, (spl66 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,sk2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 18.81/3.09 cnf(ssp101, plain, (spl5 | spl66), inference(avatar_split_clause, [status(thm)], [p1117, sdef5, sdef66])).
% 18.81/3.09 cnf(p1120, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk3,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p128, p141])).
% 18.81/3.09 fof(sdef67, definition, (spl67 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk3,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 18.81/3.09 cnf(ssp102, plain, (spl2 | spl67), inference(avatar_split_clause, [status(thm)], [p1120, sdef2, sdef67])).
% 18.81/3.09 cnf(p1122, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk3,X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p128, p155])).
% 18.81/3.09 fof(sdef68, definition, (spl68 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk3,X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 18.81/3.09 cnf(ssp103, plain, (spl2 | spl68), inference(avatar_split_clause, [status(thm)], [p1122, sdef2, sdef68])).
% 18.81/3.09 cnf(p1125, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk2,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p128, p164])).
% 18.81/3.09 fof(sdef69, definition, (spl69 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk2,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 18.81/3.09 cnf(ssp104, plain, (spl5 | spl69), inference(avatar_split_clause, [status(thm)], [p1125, sdef5, sdef69])).
% 18.81/3.09 cnf(p1128, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p128, p30])).
% 18.81/3.09 fof(sdef70, definition, (spl70 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 18.81/3.09 cnf(ssp105, plain, (spl2 | spl70), inference(avatar_split_clause, [status(thm)], [p1128, sdef2, sdef70])).
% 18.81/3.09 cnf(p1130, plain, apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk2,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p128, p30])).
% 18.81/3.09 fof(sdef71, definition, (spl71 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk2,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 18.81/3.09 cnf(ssp106, plain, (spl3 | spl71), inference(avatar_split_clause, [status(thm)], [p1130, sdef3, sdef71])).
% 18.81/3.09 cnf(p1134, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(X2,sk3) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p128, p269])).
% 18.81/3.09 fof(sdef72, definition, (spl72 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(X2,sk3) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 18.81/3.09 cnf(ssp107, plain, (spl2 | spl72), inference(avatar_split_clause, [status(thm)], [p1134, sdef2, sdef72])).
% 18.81/3.09 cnf(p1140, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(X2,sk2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p128, p365])).
% 18.81/3.09 fof(sdef73, definition, (spl73 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(X2,sk2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 18.81/3.09 cnf(ssp108, plain, (spl5 | spl73), inference(avatar_split_clause, [status(thm)], [p1140, sdef5, sdef73])).
% 18.81/3.09 cnf(p1142, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk3,X2) | distinct_lines(X2,X0), inference(resolution, [status(thm)], [p128, p407])).
% 18.81/3.09 fof(sdef74, definition, (spl74 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk3,X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl74])], [avatar_definition])).
% 18.81/3.09 cnf(ssp109, plain, (spl2 | spl74), inference(avatar_split_clause, [status(thm)], [p1142, sdef2, sdef74])).
% 18.81/3.09 cnf(p1144, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,X0) | distinct_lines(sk2,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p128, p54])).
% 18.81/3.09 fof(sdef75, definition, (spl75 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,X0) | distinct_lines(sk2,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl75])], [avatar_definition])).
% 18.81/3.09 cnf(ssp110, plain, (spl5 | spl75), inference(avatar_split_clause, [status(thm)], [p1144, sdef5, sdef75])).
% 18.81/3.09 cnf(p1147, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk3,X2) | distinct_lines(X3,X2) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p128, p54])).
% 18.81/3.09 fof(sdef76, definition, (spl76 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk3,X2) | distinct_lines(X3,X2) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl76])], [avatar_definition])).
% 18.81/3.09 cnf(ssp111, plain, (spl2 | spl76), inference(avatar_split_clause, [status(thm)], [p1147, sdef2, sdef76])).
% 18.81/3.09 cnf(p1150, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(sk3,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p128, p55])).
% 18.81/3.09 fof(sdef77, definition, (spl77 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(sk3,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl77])], [avatar_definition])).
% 18.81/3.09 cnf(ssp112, plain, (spl2 | spl77), inference(avatar_split_clause, [status(thm)], [p1150, sdef2, sdef77])).
% 18.81/3.09 cnf(p1152, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk2,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p128, p55])).
% 18.81/3.09 fof(sdef78, definition, (spl78 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk2,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl78])], [avatar_definition])).
% 18.81/3.09 cnf(ssp113, plain, (spl5 | spl78), inference(avatar_split_clause, [status(thm)], [p1152, sdef5, sdef78])).
% 18.81/3.09 cnf(p1155, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(X2,sk3), inference(resolution, [status(thm)], [p128, p428])).
% 18.81/3.09 fof(sdef79, definition, (spl79 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(X2,sk3))), introduced(definition, [new_symbols(naming, [spl79])], [avatar_definition])).
% 18.81/3.09 cnf(ssp114, plain, (spl2 | spl79), inference(avatar_split_clause, [status(thm)], [p1155, sdef2, sdef79])).
% 18.81/3.09 cnf(p1157, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk3,X2) | distinct_lines(X0,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p128, p56])).
% 18.81/3.09 fof(sdef80, definition, (spl80 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk3,X2) | distinct_lines(X0,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl80])], [avatar_definition])).
% 18.81/3.09 cnf(ssp115, plain, (spl2 | spl80), inference(avatar_split_clause, [status(thm)], [p1157, sdef2, sdef80])).
% 18.81/3.09 cnf(p1159, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk2,X2) | distinct_lines(X2,X3) | distinct_lines(X0,X3), inference(resolution, [status(thm)], [p128, p56])).
% 18.81/3.09 fof(sdef81, definition, (spl81 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk2,X2) | distinct_lines(X2,X3) | distinct_lines(X0,X3))), introduced(definition, [new_symbols(naming, [spl81])], [avatar_definition])).
% 18.81/3.09 cnf(ssp116, plain, (spl5 | spl81), inference(avatar_split_clause, [status(thm)], [p1159, sdef5, sdef81])).
% 18.81/3.09 cnf(p1162, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(X2,sk3) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p128, p513])).
% 18.81/3.09 fof(sdef82, definition, (spl82 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(X2,sk3) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl82])], [avatar_definition])).
% 18.81/3.09 cnf(ssp117, plain, (spl2 | spl82), inference(avatar_split_clause, [status(thm)], [p1162, sdef2, sdef82])).
% 18.81/3.09 cnf(p1164, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(X2,sk2) | distinct_lines(X0,X2), inference(resolution, [status(thm)], [p128, p561])).
% 18.81/3.09 fof(sdef83, definition, (spl83 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(X2,sk2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl83])], [avatar_definition])).
% 18.81/3.09 cnf(ssp118, plain, (spl5 | spl83), inference(avatar_split_clause, [status(thm)], [p1164, sdef5, sdef83])).
% 18.81/3.09 cnf(p1166, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(X2,sk2), inference(resolution, [status(thm)], [p128, p567])).
% 18.81/3.09 fof(sdef84, definition, (spl84 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(X2,sk2))), introduced(definition, [new_symbols(naming, [spl84])], [avatar_definition])).
% 18.81/3.09 cnf(ssp119, plain, (spl5 | spl84), inference(avatar_split_clause, [status(thm)], [p1166, sdef5, sdef84])).
% 18.81/3.09 cnf(p1168, plain, apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,sk3) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk3) | distinct_points(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(sk2,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p128, p143])).
% 18.81/3.09 fof(sdef85, definition, (spl85 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,sk3) | distinct_points(sk0,X1) | distinct_lines(X0,X2) | distinct_lines(sk2,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl85])], [avatar_definition])).
% 18.81/3.09 cnf(ssp120, plain, (spl5 | spl85), inference(avatar_split_clause, [status(thm)], [p1168, sdef5, sdef85])).
% 18.81/3.09 cnf(p1171, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,sk3) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p128, p143])).
% 18.81/3.09 fof(sdef86, definition, (spl86 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,sk3) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl86])], [avatar_definition])).
% 18.81/3.09 cnf(ssp121, plain, (spl2 | spl86), inference(avatar_split_clause, [status(thm)], [p1171, sdef2, sdef86])).
% 18.81/3.09 cnf(p1175, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,sk3) | distinct_lines(X2,X3) | distinct_lines(X0,X3), inference(resolution, [status(thm)], [p128, p144])).
% 18.81/3.09 fof(sdef87, definition, (spl87 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,sk3) | distinct_lines(X2,X3) | distinct_lines(X0,X3))), introduced(definition, [new_symbols(naming, [spl87])], [avatar_definition])).
% 18.81/3.09 cnf(ssp122, plain, (spl2 | spl87), inference(avatar_split_clause, [status(thm)], [p1175, sdef2, sdef87])).
% 18.81/3.09 cnf(p1186, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk2,X2) | distinct_lines(X3,X2) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p128, p238])).
% 18.81/3.09 fof(sdef88, definition, (spl88 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk2,X2) | distinct_lines(X3,X2) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl88])], [avatar_definition])).
% 18.81/3.09 cnf(ssp123, plain, (spl5 | spl88), inference(avatar_split_clause, [status(thm)], [p1186, sdef5, sdef88])).
% 18.81/3.09 cnf(p1189, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk2,X2) | distinct_lines(X0,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p128, p239])).
% 18.81/3.09 fof(sdef89, definition, (spl89 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk2,X2) | distinct_lines(X0,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl89])], [avatar_definition])).
% 18.81/3.09 cnf(ssp124, plain, (spl5 | spl89), inference(avatar_split_clause, [status(thm)], [p1189, sdef5, sdef89])).
% 18.81/3.09 cnf(p1193, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,X2) | convergent_lines(sk2,X3) | convergent_lines(X2,X3), inference(resolution, [status(thm)], [p128, p240])).
% 18.81/3.09 fof(sdef90, definition, (spl90 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,X2) | convergent_lines(sk2,X3) | convergent_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl90])], [avatar_definition])).
% 18.81/3.09 cnf(ssp125, plain, (spl5 | spl90), inference(avatar_split_clause, [status(thm)], [p1193, sdef5, sdef90])).
% 18.81/3.09 cnf(p1197, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,sk2) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p128, p243])).
% 18.81/3.09 fof(sdef91, definition, (spl91 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,sk2) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl91])], [avatar_definition])).
% 18.81/3.09 cnf(ssp126, plain, (spl5 | spl91), inference(avatar_split_clause, [status(thm)], [p1197, sdef5, sdef91])).
% 18.81/3.09 cnf(p1200, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,sk2) | distinct_lines(X2,X3) | distinct_lines(X0,X3), inference(resolution, [status(thm)], [p128, p244])).
% 18.81/3.09 fof(sdef92, definition, (spl92 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,sk2) | distinct_lines(X2,X3) | distinct_lines(X0,X3))), introduced(definition, [new_symbols(naming, [spl92])], [avatar_definition])).
% 18.81/3.09 cnf(ssp127, plain, (spl5 | spl92), inference(avatar_split_clause, [status(thm)], [p1200, sdef5, sdef92])).
% 18.81/3.09 cnf(p1203, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk3,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p128, p245])).
% 18.81/3.09 fof(sdef93, definition, (spl93 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(sk3,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl93])], [avatar_definition])).
% 18.81/3.09 cnf(ssp128, plain, (spl2 | spl93), inference(avatar_split_clause, [status(thm)], [p1203, sdef2, sdef93])).
% 18.81/3.09 cnf(p1206, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk3,X2) | distinct_lines(X3,X2) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p128, p260])).
% 18.81/3.09 fof(sdef94, definition, (spl94 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk3,X2) | distinct_lines(X3,X2) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl94])], [avatar_definition])).
% 18.81/3.09 cnf(ssp129, plain, (spl2 | spl94), inference(avatar_split_clause, [status(thm)], [p1206, sdef2, sdef94])).
% 18.81/3.09 cnf(p1209, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk3,X2) | distinct_lines(X0,X3) | distinct_lines(X2,X3), inference(resolution, [status(thm)], [p128, p261])).
% 18.81/3.09 fof(sdef95, definition, (spl95 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk3,X2) | distinct_lines(X0,X3) | distinct_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl95])], [avatar_definition])).
% 18.81/3.09 cnf(ssp130, plain, (spl2 | spl95), inference(avatar_split_clause, [status(thm)], [p1209, sdef2, sdef95])).
% 18.81/3.09 cnf(p1213, plain, apart_point_and_line(sk1,sk2) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,X2) | convergent_lines(sk3,X3) | convergent_lines(X2,X3), inference(resolution, [status(thm)], [p128, p262])).
% 18.81/3.09 fof(sdef96, definition, (spl96 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk2) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,X2) | convergent_lines(sk3,X3) | convergent_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl96])], [avatar_definition])).
% 18.81/3.09 cnf(ssp131, plain, (spl2 | spl96), inference(avatar_split_clause, [status(thm)], [p1213, sdef2, sdef96])).
% 18.81/3.09 cnf(p1216, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk2,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0), inference(resolution, [status(thm)], [p128, p265])).
% 18.81/3.09 fof(sdef97, definition, (spl97 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | convergent_lines(sk2,X2) | distinct_lines(X2,X3) | distinct_lines(X3,X0))), introduced(definition, [new_symbols(naming, [spl97])], [avatar_definition])).
% 18.81/3.09 cnf(ssp132, plain, (spl5 | spl97), inference(avatar_split_clause, [status(thm)], [p1216, sdef5, sdef97])).
% 18.81/3.09 cnf(p1218, plain, apart_point_and_line(sk1,sk3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,X0) | convergent_lines(sk2,X3) | convergent_lines(X2,X3), inference(resolution, [status(thm)], [p128, p266])).
% 18.81/3.09 fof(sdef98, definition, (spl98 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,sk3) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,X0) | convergent_lines(sk2,X3) | convergent_lines(X2,X3))), introduced(definition, [new_symbols(naming, [spl98])], [avatar_definition])).
% 18.81/3.09 cnf(ssp133, plain, (spl5 | spl98), inference(avatar_split_clause, [status(thm)], [p1218, sdef5, sdef98])).
% 18.81/3.09 fof(f7, axiom, ! [X,Y,Z] : ( convergent_lines(X,Y) => ( ( apart_point_and_line(Z,X) | apart_point_and_line(Z,Y) ) => distinct_points(Z,intersection_point(X,Y)) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con2)).
% 18.81/3.09 fof(f7_nnf, plain, ! [X,Y,Z] : ((~(convergent_lines(X,Y)) | ((~(apart_point_and_line(Z,X)) & ~(apart_point_and_line(Z,Y))) | distinct_points(Z,intersection_point(X,Y))))), inference(nnf_transformation, [status(thm)], [f7])).
% 18.81/3.09 fof(f7_sk, plain, ! [X,Y,Z] : ((~(convergent_lines(X,Y)) | ((~(apart_point_and_line(Z,X)) & ~(apart_point_and_line(Z,Y))) | distinct_points(Z,intersection_point(X,Y))))), inference(skolemisation, [status(esa)], [f7_nnf])).
% 18.81/3.09 cnf(c8, plain, ~convergent_lines(X0,X1) | ~apart_point_and_line(X2,X0) | distinct_points(X2,intersection_point(X0,X1)), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 18.81/3.09 cnf(p101, plain, convergent_lines(sk2,X0) | ~apart_point_and_line(X1,X0) | distinct_points(X1,intersection_point(X0,sk3)), inference(resolution, [status(thm)], [p87, c8])).
% 18.81/3.09 cnf(p1226, plain, (convergent_lines(sk2,line_connecting(sk0,sk1)) | distinct_points(sk0,intersection_point(line_connecting(sk0,sk1),sk3)) | ~spl1), inference(resolution, [status(thm)], [p920, p101])).
% 18.81/3.09 fof(sdef99, definition, (spl99 <=> (convergent_lines(sk2,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl99])], [avatar_definition])).
% 18.81/3.09 fof(sdef100, definition, (spl100 <=> (distinct_points(sk0,intersection_point(line_connecting(sk0,sk1),sk3)))), introduced(definition, [new_symbols(naming, [spl100])], [avatar_definition])).
% 18.81/3.09 cnf(ssp134, plain, (~spl1 | spl99 | spl100), inference(avatar_split_clause, [status(thm)], [p1226, sdef99, sdef100])).
% 18.81/3.09 cnf(c9, plain, ~convergent_lines(X0,X1) | ~apart_point_and_line(X2,X1) | distinct_points(X2,intersection_point(X0,X1)), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 18.81/3.09 cnf(p104, plain, ~apart_point_and_line(X0,X1) | distinct_points(X0,intersection_point(sk3,X1)) | convergent_lines(sk2,X1), inference(resolution, [status(thm)], [c9, p36])).
% 18.81/3.09 cnf(p1229, plain, (distinct_points(sk0,intersection_point(sk3,line_connecting(sk0,sk1))) | convergent_lines(sk2,line_connecting(sk0,sk1)) | ~spl1), inference(resolution, [status(thm)], [p920, p104])).
% 18.81/3.09 fof(sdef101, definition, (spl101 <=> (distinct_points(sk0,intersection_point(sk3,line_connecting(sk0,sk1))))), introduced(definition, [new_symbols(naming, [spl101])], [avatar_definition])).
% 18.81/3.09 cnf(ssp135, plain, (~spl1 | spl99 | spl101), inference(avatar_split_clause, [status(thm)], [p1229, sdef99, sdef101])).
% 18.81/3.09 cnf(p105, plain, ~apart_point_and_line(X0,X1) | distinct_points(X0,intersection_point(sk2,X1)) | distinct_lines(sk3,X1), inference(resolution, [status(thm)], [c9, p37])).
% 18.81/3.09 cnf(p1231, plain, (distinct_points(sk0,intersection_point(sk2,line_connecting(sk0,sk1))) | distinct_lines(sk3,line_connecting(sk0,sk1)) | ~spl1), inference(resolution, [status(thm)], [p920, p105])).
% 18.81/3.09 fof(sdef102, definition, (spl102 <=> (distinct_points(sk0,intersection_point(sk2,line_connecting(sk0,sk1))))), introduced(definition, [new_symbols(naming, [spl102])], [avatar_definition])).
% 18.81/3.09 fof(sdef103, definition, (spl103 <=> (distinct_lines(sk3,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl103])], [avatar_definition])).
% 18.81/3.09 cnf(ssp136, plain, (~spl1 | spl102 | spl103), inference(avatar_split_clause, [status(thm)], [p1231, sdef102, sdef103])).
% 18.81/3.09 cnf(p109, plain, ~apart_point_and_line(X0,X1) | distinct_points(X0,intersection_point(sk2,X1)) | convergent_lines(X1,sk3), inference(resolution, [status(thm)], [c9, p87])).
% 18.81/3.09 cnf(p1234, plain, (distinct_points(sk0,intersection_point(sk2,line_connecting(sk0,sk1))) | convergent_lines(line_connecting(sk0,sk1),sk3) | ~spl1), inference(resolution, [status(thm)], [p920, p109])).
% 18.81/3.09 fof(sdef104, definition, (spl104 <=> (convergent_lines(line_connecting(sk0,sk1),sk3))), introduced(definition, [new_symbols(naming, [spl104])], [avatar_definition])).
% 18.81/3.09 cnf(ssp137, plain, (~spl1 | spl102 | spl104), inference(avatar_split_clause, [status(thm)], [p1234, sdef102, sdef104])).
% 18.81/3.09 cnf(p114, plain, distinct_lines(X0,sk3) | ~apart_point_and_line(X1,X0) | distinct_points(X1,intersection_point(sk2,X0)), inference(resolution, [status(thm)], [p98, c9])).
% 18.81/3.09 cnf(p1236, plain, (distinct_lines(line_connecting(sk0,sk1),sk3) | distinct_points(sk0,intersection_point(sk2,line_connecting(sk0,sk1))) | ~spl1), inference(resolution, [status(thm)], [p920, p114])).
% 18.81/3.09 fof(sdef105, definition, (spl105 <=> (distinct_lines(line_connecting(sk0,sk1),sk3))), introduced(definition, [new_symbols(naming, [spl105])], [avatar_definition])).
% 18.81/3.09 cnf(ssp138, plain, (~spl1 | spl102 | spl105), inference(avatar_split_clause, [status(thm)], [p1236, sdef102, sdef105])).
% 18.81/3.09 cnf(p125, plain, distinct_lines(sk3,X0) | ~apart_point_and_line(X1,X0) | distinct_points(X1,intersection_point(X0,sk2)), inference(resolution, [status(thm)], [p115, c8])).
% 18.81/3.09 cnf(p1238, plain, (distinct_lines(sk3,line_connecting(sk0,sk1)) | distinct_points(sk0,intersection_point(line_connecting(sk0,sk1),sk2)) | ~spl1), inference(resolution, [status(thm)], [p920, p125])).
% 18.81/3.09 fof(sdef106, definition, (spl106 <=> (distinct_points(sk0,intersection_point(line_connecting(sk0,sk1),sk2)))), introduced(definition, [new_symbols(naming, [spl106])], [avatar_definition])).
% 18.81/3.09 cnf(ssp139, plain, (~spl1 | spl103 | spl106), inference(avatar_split_clause, [status(thm)], [p1238, sdef103, sdef106])).
% 18.81/3.09 cnf(p191, plain, convergent_lines(X0,sk2) | ~apart_point_and_line(X1,X0) | distinct_points(X1,intersection_point(X0,sk3)), inference(resolution, [status(thm)], [p177, c8])).
% 18.81/3.09 cnf(p1240, plain, (convergent_lines(line_connecting(sk0,sk1),sk2) | distinct_points(sk0,intersection_point(line_connecting(sk0,sk1),sk3)) | ~spl1), inference(resolution, [status(thm)], [p920, p191])).
% 18.81/3.09 fof(sdef107, definition, (spl107 <=> (convergent_lines(line_connecting(sk0,sk1),sk2))), introduced(definition, [new_symbols(naming, [spl107])], [avatar_definition])).
% 18.81/3.09 cnf(ssp140, plain, (~spl1 | spl100 | spl107), inference(avatar_split_clause, [status(thm)], [p1240, sdef100, sdef107])).
% 18.81/3.09 cnf(p189, plain, convergent_lines(X0,sk2) | distinct_lines(X0,sk3), inference(resolution, [status(thm)], [p177, c13])).
% 18.81/3.09 cnf(p195, plain, distinct_lines(X0,sk3) | ~apart_point_and_line(X1,X0) | distinct_points(X1,intersection_point(X0,sk2)), inference(resolution, [status(thm)], [p189, c8])).
% 18.81/3.09 cnf(p1242, plain, (distinct_lines(line_connecting(sk0,sk1),sk3) | distinct_points(sk0,intersection_point(line_connecting(sk0,sk1),sk2)) | ~spl1), inference(resolution, [status(thm)], [p920, p195])).
% 18.81/3.09 cnf(ssp141, plain, (~spl1 | spl105 | spl106), inference(avatar_split_clause, [status(thm)], [p1242, sdef105, sdef106])).
% 18.81/3.09 cnf(p289, plain, distinct_lines(X0,sk2) | ~apart_point_and_line(X1,X0) | distinct_points(X1,intersection_point(X0,sk3)), inference(resolution, [status(thm)], [p276, c8])).
% 18.81/3.09 cnf(p1243, plain, (distinct_lines(line_connecting(sk0,sk1),sk2) | distinct_points(sk0,intersection_point(line_connecting(sk0,sk1),sk3)) | ~spl1), inference(resolution, [status(thm)], [p920, p289])).
% 18.81/3.09 fof(sdef108, definition, (spl108 <=> (distinct_lines(line_connecting(sk0,sk1),sk2))), introduced(definition, [new_symbols(naming, [spl108])], [avatar_definition])).
% 18.81/3.09 cnf(ssp142, plain, (~spl1 | spl100 | spl108), inference(avatar_split_clause, [status(thm)], [p1243, sdef100, sdef108])).
% 18.81/3.09 cnf(p304, plain, convergent_lines(sk3,X0) | ~apart_point_and_line(X1,X0) | distinct_points(X1,intersection_point(X0,sk2)), inference(resolution, [status(thm)], [p291, c8])).
% 18.81/3.09 cnf(p1245, plain, (convergent_lines(sk3,line_connecting(sk0,sk1)) | distinct_points(sk0,intersection_point(line_connecting(sk0,sk1),sk2)) | ~spl1), inference(resolution, [status(thm)], [p920, p304])).
% 18.81/3.09 fof(sdef109, definition, (spl109 <=> (convergent_lines(sk3,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl109])], [avatar_definition])).
% 18.81/3.09 cnf(ssp143, plain, (~spl1 | spl106 | spl109), inference(avatar_split_clause, [status(thm)], [p1245, sdef106, sdef109])).
% 18.81/3.09 cnf(p307, plain, convergent_lines(X0,sk2) | ~apart_point_and_line(X1,X0) | distinct_points(X1,intersection_point(sk3,X0)), inference(resolution, [status(thm)], [p291, c9])).
% 18.81/3.09 cnf(p1247, plain, (convergent_lines(line_connecting(sk0,sk1),sk2) | distinct_points(sk0,intersection_point(sk3,line_connecting(sk0,sk1))) | ~spl1), inference(resolution, [status(thm)], [p920, p307])).
% 18.81/3.09 cnf(ssp144, plain, (~spl1 | spl101 | spl107), inference(avatar_split_clause, [status(thm)], [p1247, sdef101, sdef107])).
% 18.81/3.09 cnf(p302, plain, convergent_lines(sk3,X0) | distinct_lines(X0,sk2), inference(resolution, [status(thm)], [p291, c13])).
% 18.81/3.09 cnf(p325, plain, distinct_lines(X0,sk2) | ~apart_point_and_line(X1,X0) | distinct_points(X1,intersection_point(sk3,X0)), inference(resolution, [status(thm)], [p302, c9])).
% 18.81/3.09 cnf(p1248, plain, (distinct_lines(line_connecting(sk0,sk1),sk2) | distinct_points(sk0,intersection_point(sk3,line_connecting(sk0,sk1))) | ~spl1), inference(resolution, [status(thm)], [p920, p325])).
% 18.81/3.09 cnf(ssp145, plain, (~spl1 | spl101 | spl108), inference(avatar_split_clause, [status(thm)], [p1248, sdef101, sdef108])).
% 18.81/3.09 cnf(p96, plain, convergent_lines(sk2,X0) | convergent_lines(sk3,X1) | ~apart_point_and_line(X2,X0) | distinct_points(X2,intersection_point(X0,X1)), inference(resolution, [status(thm)], [p38, c8])).
% 18.81/3.09 cnf(p1249, plain, (convergent_lines(sk2,line_connecting(sk0,sk1)) | convergent_lines(sk3,X0) | distinct_points(sk0,intersection_point(line_connecting(sk0,sk1),X0)) | ~spl1), inference(resolution, [status(thm)], [p920, p96])).
% 18.81/3.09 fof(sdef110, definition, (spl110 <=> (convergent_lines(sk3,X0) | distinct_points(sk0,intersection_point(line_connecting(sk0,sk1),X0)))), introduced(definition, [new_symbols(naming, [spl110])], [avatar_definition])).
% 18.81/3.09 cnf(ssp146, plain, (~spl1 | spl99 | spl110), inference(avatar_split_clause, [status(thm)], [p1249, sdef99, sdef110])).
% 18.81/3.09 cnf(p106, plain, ~apart_point_and_line(X0,X1) | distinct_points(X0,intersection_point(sk2,X1)) | convergent_lines(sk3,X2) | convergent_lines(X1,X2), inference(resolution, [status(thm)], [c9, p38])).
% 18.81/3.09 cnf(p1251, plain, (distinct_points(sk0,intersection_point(sk2,line_connecting(sk0,sk1))) | convergent_lines(sk3,X0) | convergent_lines(line_connecting(sk0,sk1),X0) | ~spl1), inference(resolution, [status(thm)], [p920, p106])).
% 18.81/3.09 fof(sdef111, definition, (spl111 <=> (convergent_lines(sk3,X0) | convergent_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl111])], [avatar_definition])).
% 18.81/3.09 cnf(ssp147, plain, (~spl1 | spl102 | spl111), inference(avatar_split_clause, [status(thm)], [p1251, sdef102, sdef111])).
% 18.81/3.09 cnf(p107, plain, ~apart_point_and_line(X0,X1) | distinct_points(X0,intersection_point(sk3,X1)) | convergent_lines(sk2,X2) | convergent_lines(X2,X1), inference(resolution, [status(thm)], [c9, p38])).
% 18.81/3.09 cnf(p1253, plain, (distinct_points(sk0,intersection_point(sk3,line_connecting(sk0,sk1))) | convergent_lines(sk2,X0) | convergent_lines(X0,line_connecting(sk0,sk1)) | ~spl1), inference(resolution, [status(thm)], [p920, p107])).
% 18.81/3.09 fof(sdef112, definition, (spl112 <=> (convergent_lines(sk2,X0) | convergent_lines(X0,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl112])], [avatar_definition])).
% 18.81/3.09 cnf(ssp148, plain, (~spl1 | spl101 | spl112), inference(avatar_split_clause, [status(thm)], [p1253, sdef101, sdef112])).
% 18.81/3.09 cnf(p108, plain, ~apart_point_and_line(X0,X1) | distinct_points(X0,intersection_point(X2,X1)) | convergent_lines(sk2,X2) | convergent_lines(sk3,X1), inference(resolution, [status(thm)], [c9, p38])).
% 18.81/3.09 cnf(p1255, plain, (distinct_points(sk0,intersection_point(X0,line_connecting(sk0,sk1))) | convergent_lines(sk2,X0) | convergent_lines(sk3,line_connecting(sk0,sk1)) | ~spl1), inference(resolution, [status(thm)], [p920, p108])).
% 18.81/3.09 fof(sdef113, definition, (spl113 <=> (distinct_points(sk0,intersection_point(X0,line_connecting(sk0,sk1))) | convergent_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl113])], [avatar_definition])).
% 18.81/3.09 cnf(ssp149, plain, (~spl1 | spl109 | spl113), inference(avatar_split_clause, [status(thm)], [p1255, sdef109, sdef113])).
% 18.81/3.09 cnf(p121, plain, distinct_lines(sk3,X0) | convergent_lines(sk2,X1) | ~apart_point_and_line(X2,X0) | distinct_points(X2,intersection_point(X0,X1)), inference(resolution, [status(thm)], [p40, c8])).
% 18.81/3.09 cnf(p1257, plain, (distinct_lines(sk3,line_connecting(sk0,sk1)) | convergent_lines(sk2,X0) | distinct_points(sk0,intersection_point(line_connecting(sk0,sk1),X0)) | ~spl1), inference(resolution, [status(thm)], [p920, p121])).
% 18.81/3.09 fof(sdef114, definition, (spl114 <=> (convergent_lines(sk2,X0) | distinct_points(sk0,intersection_point(line_connecting(sk0,sk1),X0)))), introduced(definition, [new_symbols(naming, [spl114])], [avatar_definition])).
% 18.81/3.09 cnf(ssp150, plain, (~spl1 | spl103 | spl114), inference(avatar_split_clause, [status(thm)], [p1257, sdef103, sdef114])).
% 18.81/3.09 cnf(p122, plain, distinct_lines(sk3,X0) | convergent_lines(X0,X1) | ~apart_point_and_line(X2,X1) | distinct_points(X2,intersection_point(sk2,X1)), inference(resolution, [status(thm)], [p40, c9])).
% 18.81/3.09 cnf(p1259, plain, (distinct_lines(sk3,X0) | convergent_lines(X0,line_connecting(sk0,sk1)) | distinct_points(sk0,intersection_point(sk2,line_connecting(sk0,sk1))) | ~spl1), inference(resolution, [status(thm)], [p920, p122])).
% 18.81/3.09 fof(sdef115, definition, (spl115 <=> (distinct_lines(sk3,X0) | convergent_lines(X0,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl115])], [avatar_definition])).
% 18.81/3.09 cnf(ssp151, plain, (~spl1 | spl102 | spl115), inference(avatar_split_clause, [status(thm)], [p1259, sdef102, sdef115])).
% 18.81/3.09 cnf(p123, plain, distinct_lines(sk3,X0) | convergent_lines(sk2,X1) | ~apart_point_and_line(X2,X1) | distinct_points(X2,intersection_point(X0,X1)), inference(resolution, [status(thm)], [p40, c9])).
% 18.81/3.09 cnf(p1261, plain, (distinct_lines(sk3,X0) | convergent_lines(sk2,line_connecting(sk0,sk1)) | distinct_points(sk0,intersection_point(X0,line_connecting(sk0,sk1))) | ~spl1), inference(resolution, [status(thm)], [p920, p123])).
% 18.81/3.09 fof(sdef116, definition, (spl116 <=> (distinct_lines(sk3,X0) | distinct_points(sk0,intersection_point(X0,line_connecting(sk0,sk1))))), introduced(definition, [new_symbols(naming, [spl116])], [avatar_definition])).
% 18.81/3.09 cnf(ssp152, plain, (~spl1 | spl99 | spl116), inference(avatar_split_clause, [status(thm)], [p1261, sdef99, sdef116])).
% 18.81/3.09 cnf(p1267, plain, (convergent_lines(sk2,line_connecting(sk0,sk1)) | distinct_points(sk1,intersection_point(line_connecting(sk0,sk1),sk3)) | ~spl3), inference(resolution, [status(thm)], [p922, p101])).
% 18.81/3.09 fof(sdef117, definition, (spl117 <=> (distinct_points(sk1,intersection_point(line_connecting(sk0,sk1),sk3)))), introduced(definition, [new_symbols(naming, [spl117])], [avatar_definition])).
% 18.81/3.09 cnf(ssp153, plain, (~spl3 | spl99 | spl117), inference(avatar_split_clause, [status(thm)], [p1267, sdef99, sdef117])).
% 18.81/3.09 cnf(p1269, plain, (distinct_points(sk1,intersection_point(sk3,line_connecting(sk0,sk1))) | convergent_lines(sk2,line_connecting(sk0,sk1)) | ~spl3), inference(resolution, [status(thm)], [p922, p104])).
% 18.81/3.09 fof(sdef118, definition, (spl118 <=> (distinct_points(sk1,intersection_point(sk3,line_connecting(sk0,sk1))))), introduced(definition, [new_symbols(naming, [spl118])], [avatar_definition])).
% 18.81/3.09 cnf(ssp154, plain, (~spl3 | spl99 | spl118), inference(avatar_split_clause, [status(thm)], [p1269, sdef99, sdef118])).
% 18.81/3.09 cnf(p1271, plain, (distinct_points(sk1,intersection_point(sk2,line_connecting(sk0,sk1))) | distinct_lines(sk3,line_connecting(sk0,sk1)) | ~spl3), inference(resolution, [status(thm)], [p922, p105])).
% 18.81/3.09 fof(sdef119, definition, (spl119 <=> (distinct_points(sk1,intersection_point(sk2,line_connecting(sk0,sk1))))), introduced(definition, [new_symbols(naming, [spl119])], [avatar_definition])).
% 18.81/3.09 cnf(ssp155, plain, (~spl3 | spl103 | spl119), inference(avatar_split_clause, [status(thm)], [p1271, sdef103, sdef119])).
% 18.81/3.09 cnf(p1273, plain, (distinct_points(sk1,intersection_point(sk2,line_connecting(sk0,sk1))) | convergent_lines(line_connecting(sk0,sk1),sk3) | ~spl3), inference(resolution, [status(thm)], [p922, p109])).
% 18.81/3.09 cnf(ssp156, plain, (~spl3 | spl104 | spl119), inference(avatar_split_clause, [status(thm)], [p1273, sdef104, sdef119])).
% 18.81/3.09 cnf(p1274, plain, (distinct_lines(line_connecting(sk0,sk1),sk3) | distinct_points(sk1,intersection_point(sk2,line_connecting(sk0,sk1))) | ~spl3), inference(resolution, [status(thm)], [p922, p114])).
% 18.81/3.09 cnf(ssp157, plain, (~spl3 | spl105 | spl119), inference(avatar_split_clause, [status(thm)], [p1274, sdef105, sdef119])).
% 18.81/3.09 cnf(p1275, plain, (distinct_lines(sk3,line_connecting(sk0,sk1)) | distinct_points(sk1,intersection_point(line_connecting(sk0,sk1),sk2)) | ~spl3), inference(resolution, [status(thm)], [p922, p125])).
% 18.81/3.09 fof(sdef120, definition, (spl120 <=> (distinct_points(sk1,intersection_point(line_connecting(sk0,sk1),sk2)))), introduced(definition, [new_symbols(naming, [spl120])], [avatar_definition])).
% 18.81/3.09 cnf(ssp158, plain, (~spl3 | spl103 | spl120), inference(avatar_split_clause, [status(thm)], [p1275, sdef103, sdef120])).
% 18.81/3.09 cnf(p1277, plain, (convergent_lines(line_connecting(sk0,sk1),sk2) | distinct_points(sk1,intersection_point(line_connecting(sk0,sk1),sk3)) | ~spl3), inference(resolution, [status(thm)], [p922, p191])).
% 18.81/3.09 cnf(ssp159, plain, (~spl3 | spl107 | spl117), inference(avatar_split_clause, [status(thm)], [p1277, sdef107, sdef117])).
% 18.81/3.09 cnf(p1278, plain, (distinct_lines(line_connecting(sk0,sk1),sk3) | distinct_points(sk1,intersection_point(line_connecting(sk0,sk1),sk2)) | ~spl3), inference(resolution, [status(thm)], [p922, p195])).
% 18.81/3.09 cnf(ssp160, plain, (~spl3 | spl105 | spl120), inference(avatar_split_clause, [status(thm)], [p1278, sdef105, sdef120])).
% 18.81/3.09 cnf(p1279, plain, (distinct_lines(line_connecting(sk0,sk1),sk2) | distinct_points(sk1,intersection_point(line_connecting(sk0,sk1),sk3)) | ~spl3), inference(resolution, [status(thm)], [p922, p289])).
% 18.81/3.09 cnf(ssp161, plain, (~spl3 | spl108 | spl117), inference(avatar_split_clause, [status(thm)], [p1279, sdef108, sdef117])).
% 18.81/3.09 cnf(p1280, plain, (convergent_lines(sk3,line_connecting(sk0,sk1)) | distinct_points(sk1,intersection_point(line_connecting(sk0,sk1),sk2)) | ~spl3), inference(resolution, [status(thm)], [p922, p304])).
% 18.81/3.09 cnf(ssp162, plain, (~spl3 | spl109 | spl120), inference(avatar_split_clause, [status(thm)], [p1280, sdef109, sdef120])).
% 18.81/3.09 cnf(p1281, plain, (convergent_lines(line_connecting(sk0,sk1),sk2) | distinct_points(sk1,intersection_point(sk3,line_connecting(sk0,sk1))) | ~spl3), inference(resolution, [status(thm)], [p922, p307])).
% 18.81/3.09 cnf(ssp163, plain, (~spl3 | spl107 | spl118), inference(avatar_split_clause, [status(thm)], [p1281, sdef107, sdef118])).
% 18.81/3.09 cnf(p1282, plain, (distinct_lines(line_connecting(sk0,sk1),sk2) | distinct_points(sk1,intersection_point(sk3,line_connecting(sk0,sk1))) | ~spl3), inference(resolution, [status(thm)], [p922, p325])).
% 18.81/3.09 cnf(ssp164, plain, (~spl3 | spl108 | spl118), inference(avatar_split_clause, [status(thm)], [p1282, sdef108, sdef118])).
% 18.81/3.09 cnf(p1283, plain, (convergent_lines(sk2,line_connecting(sk0,sk1)) | convergent_lines(sk3,X0) | distinct_points(sk1,intersection_point(line_connecting(sk0,sk1),X0)) | ~spl3), inference(resolution, [status(thm)], [p922, p96])).
% 18.81/3.09 fof(sdef121, definition, (spl121 <=> (convergent_lines(sk3,X0) | distinct_points(sk1,intersection_point(line_connecting(sk0,sk1),X0)))), introduced(definition, [new_symbols(naming, [spl121])], [avatar_definition])).
% 18.81/3.09 cnf(ssp165, plain, (~spl3 | spl99 | spl121), inference(avatar_split_clause, [status(thm)], [p1283, sdef99, sdef121])).
% 18.81/3.09 cnf(p1285, plain, (distinct_points(sk1,intersection_point(sk2,line_connecting(sk0,sk1))) | convergent_lines(sk3,X0) | convergent_lines(line_connecting(sk0,sk1),X0) | ~spl3), inference(resolution, [status(thm)], [p922, p106])).
% 18.81/3.09 cnf(ssp166, plain, (~spl3 | spl111 | spl119), inference(avatar_split_clause, [status(thm)], [p1285, sdef111, sdef119])).
% 18.81/3.09 cnf(p1286, plain, (distinct_points(sk1,intersection_point(sk3,line_connecting(sk0,sk1))) | convergent_lines(sk2,X0) | convergent_lines(X0,line_connecting(sk0,sk1)) | ~spl3), inference(resolution, [status(thm)], [p922, p107])).
% 18.81/3.09 cnf(ssp167, plain, (~spl3 | spl112 | spl118), inference(avatar_split_clause, [status(thm)], [p1286, sdef112, sdef118])).
% 18.81/3.09 cnf(p1287, plain, (distinct_points(sk1,intersection_point(X0,line_connecting(sk0,sk1))) | convergent_lines(sk2,X0) | convergent_lines(sk3,line_connecting(sk0,sk1)) | ~spl3), inference(resolution, [status(thm)], [p922, p108])).
% 18.81/3.09 fof(sdef122, definition, (spl122 <=> (distinct_points(sk1,intersection_point(X0,line_connecting(sk0,sk1))) | convergent_lines(sk2,X0))), introduced(definition, [new_symbols(naming, [spl122])], [avatar_definition])).
% 18.81/3.09 cnf(ssp168, plain, (~spl3 | spl109 | spl122), inference(avatar_split_clause, [status(thm)], [p1287, sdef109, sdef122])).
% 18.81/3.09 cnf(p1289, plain, (distinct_lines(sk3,line_connecting(sk0,sk1)) | convergent_lines(sk2,X0) | distinct_points(sk1,intersection_point(line_connecting(sk0,sk1),X0)) | ~spl3), inference(resolution, [status(thm)], [p922, p121])).
% 18.81/3.09 fof(sdef123, definition, (spl123 <=> (convergent_lines(sk2,X0) | distinct_points(sk1,intersection_point(line_connecting(sk0,sk1),X0)))), introduced(definition, [new_symbols(naming, [spl123])], [avatar_definition])).
% 18.81/3.09 cnf(ssp169, plain, (~spl3 | spl103 | spl123), inference(avatar_split_clause, [status(thm)], [p1289, sdef103, sdef123])).
% 18.81/3.09 cnf(p1291, plain, (distinct_lines(sk3,X0) | convergent_lines(X0,line_connecting(sk0,sk1)) | distinct_points(sk1,intersection_point(sk2,line_connecting(sk0,sk1))) | ~spl3), inference(resolution, [status(thm)], [p922, p122])).
% 18.81/3.09 cnf(ssp170, plain, (~spl3 | spl115 | spl119), inference(avatar_split_clause, [status(thm)], [p1291, sdef115, sdef119])).
% 18.81/3.09 cnf(p1292, plain, (distinct_lines(sk3,X0) | convergent_lines(sk2,line_connecting(sk0,sk1)) | distinct_points(sk1,intersection_point(X0,line_connecting(sk0,sk1))) | ~spl3), inference(resolution, [status(thm)], [p922, p123])).
% 18.81/3.09 fof(sdef124, definition, (spl124 <=> (distinct_lines(sk3,X0) | distinct_points(sk1,intersection_point(X0,line_connecting(sk0,sk1))))), introduced(definition, [new_symbols(naming, [spl124])], [avatar_definition])).
% 18.81/3.09 cnf(ssp171, plain, (~spl3 | spl99 | spl124), inference(avatar_split_clause, [status(thm)], [p1292, sdef99, sdef124])).
% 18.81/3.09 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, sct0, sct1, sct2, sct3])).
% 18.81/3.09 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------