%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO187+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:17:21 PM UTC 2026
% Result : Theorem 24.69s 3.66s
% Output : Proof 24.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO187+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 11:21:42 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 24.69/3.66 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 24.69/3.66 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 24.69/3.66 fof(sdef2, definition, (spl2 <=> (distinct_points(sk2,sk2))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 24.69/3.66 cnf(p647, plain, (distinct_points(sk2,sk2) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 24.69/3.66 fof(f0, axiom, ! [X] : ~ distinct_points(X,X), file('/export/starexec/sandbox/benchmark/theBenchmark.p', apart1)).
% 24.69/3.66 fof(f0_nnf, plain, ! [X] : (~(distinct_points(X,X))), inference(nnf_transformation, [status(thm)], [f0])).
% 24.69/3.66 fof(f0_sk, plain, ! [X] : (~(distinct_points(X,X))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 24.69/3.66 cnf(c0, plain, ~distinct_points(X0,X0), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 24.69/3.66 cnf(p696, plain, ($false | ~spl2), inference(resolution, [status(thm)], [p647, c0])).
% 24.69/3.66 cnf(sct0, plain, (~spl2), inference(avatar_contradiction_clause, [status(thm)], [p696])).
% 24.69/3.66 fof(sdef21, definition, (spl21 <=> (apart_point_and_line(sk0,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 24.69/3.66 cnf(p698, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 24.69/3.66 fof(f6, axiom, ! [X,Y] : ( distinct_points(X,Y) => ~ apart_point_and_line(X,line_connecting(X,Y)) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ci1)).
% 24.69/3.66 fof(f6_nnf, plain, ! [X,Y] : ((~(distinct_points(X,Y)) | ~(apart_point_and_line(X,line_connecting(X,Y))))), inference(nnf_transformation, [status(thm)], [f6])).
% 24.69/3.66 fof(f6_sk, plain, ! [X,Y] : ((~(distinct_points(X,Y)) | ~(apart_point_and_line(X,line_connecting(X,Y))))), inference(skolemisation, [status(esa)], [f6_nnf])).
% 24.69/3.66 cnf(c6, plain, ~distinct_points(X0,X1) | ~apart_point_and_line(X0,line_connecting(X0,X1)), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 24.69/3.66 fof(f14, conjecture, ! [X,Y,U,V] : ( ( distinct_points(X,Y) & distinct_points(U,V) & ~ apart_point_and_line(X,line_connecting(U,V)) & ~ apart_point_and_line(Y,line_connecting(U,V)) ) => ( ~ apart_point_and_line(U,line_connecting(X,Y)) & ~ apart_point_and_line(V,line_connecting(X,Y)) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 24.69/3.66 fof(f14_neg, negated_conjecture, ~(! [X,Y,U,V] : ( ( distinct_points(X,Y) & distinct_points(U,V) & ~ apart_point_and_line(X,line_connecting(U,V)) & ~ apart_point_and_line(Y,line_connecting(U,V)) ) => ( ~ apart_point_and_line(U,line_connecting(X,Y)) & ~ apart_point_and_line(V,line_connecting(X,Y)) ) )), inference(negated_conjecture, [status(cth)], [f14])).
% 24.69/3.66 fof(f14_nnf, plain, ? [X,Y,U,V] : (((((distinct_points(X,Y) & distinct_points(U,V)) & ~(apart_point_and_line(X,line_connecting(U,V)))) & ~(apart_point_and_line(Y,line_connecting(U,V)))) & (apart_point_and_line(U,line_connecting(X,Y)) | apart_point_and_line(V,line_connecting(X,Y))))), inference(nnf_transformation, [status(thm)], [f14_neg])).
% 24.69/3.66 fof(f14_sk, plain, ((((distinct_points(sk0,sk1) & distinct_points(sk2,sk3)) & ~(apart_point_and_line(sk0,line_connecting(sk2,sk3)))) & ~(apart_point_and_line(sk1,line_connecting(sk2,sk3)))) & (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk3,line_connecting(sk0,sk1)))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2,sk3])], [f14_nnf])).
% 24.69/3.66 cnf(c14, plain, distinct_points(sk0,sk1), inference(cnf_transformation, [status(esa)], [f14_sk])).
% 24.69/3.66 cnf(p45, plain, ~apart_point_and_line(sk0,line_connecting(sk0,sk1)), inference(resolution, [status(thm)], [c6, c14])).
% 24.69/3.66 cnf(p705, plain, ($false | ~spl21), inference(resolution, [status(thm)], [p698, p45])).
% 24.69/3.66 cnf(sct1, plain, (~spl21), inference(avatar_contradiction_clause, [status(thm)], [p705])).
% 24.69/3.66 fof(sdef23, definition, (spl23 <=> (apart_point_and_line(sk1,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 24.69/3.66 cnf(p700, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | ~spl23), inference(avatar_component_clause, [status(thm)], [sdef23])).
% 24.69/3.66 fof(f7, axiom, ! [X,Y] : ( distinct_points(X,Y) => ~ apart_point_and_line(Y,line_connecting(X,Y)) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ci2)).
% 24.69/3.66 fof(f7_nnf, plain, ! [X,Y] : ((~(distinct_points(X,Y)) | ~(apart_point_and_line(Y,line_connecting(X,Y))))), inference(nnf_transformation, [status(thm)], [f7])).
% 24.69/3.66 fof(f7_sk, plain, ! [X,Y] : ((~(distinct_points(X,Y)) | ~(apart_point_and_line(Y,line_connecting(X,Y))))), inference(skolemisation, [status(esa)], [f7_nnf])).
% 24.69/3.66 cnf(c7, plain, ~distinct_points(X0,X1) | ~apart_point_and_line(X1,line_connecting(X0,X1)), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 24.69/3.66 cnf(p69, plain, ~apart_point_and_line(sk1,line_connecting(sk0,sk1)), inference(resolution, [status(thm)], [c7, c14])).
% 24.69/3.66 cnf(p706, plain, ($false | ~spl23), inference(resolution, [status(thm)], [p700, p69])).
% 24.69/3.66 cnf(sct2, plain, (~spl23), inference(avatar_contradiction_clause, [status(thm)], [p706])).
% 24.69/3.66 fof(sdef26, definition, (spl26 <=> (apart_point_and_line(sk0,line_connecting(sk2,sk3)))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 24.69/3.66 cnf(p709, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk3)) | ~spl26), inference(avatar_component_clause, [status(thm)], [sdef26])).
% 24.69/3.66 cnf(c16, plain, ~apart_point_and_line(sk0,line_connecting(sk2,sk3)), inference(cnf_transformation, [status(esa)], [f14_sk])).
% 24.69/3.66 cnf(p711, plain, ($false | ~spl26), inference(resolution, [status(thm)], [p709, c16])).
% 24.69/3.66 cnf(sct3, plain, (~spl26), inference(avatar_contradiction_clause, [status(thm)], [p711])).
% 24.69/3.66 fof(sdef27, definition, (spl27 <=> (apart_point_and_line(sk1,line_connecting(sk2,sk3)))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 24.69/3.66 cnf(p710, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk3)) | ~spl27), inference(avatar_component_clause, [status(thm)], [sdef27])).
% 24.69/3.66 cnf(c17, plain, ~apart_point_and_line(sk1,line_connecting(sk2,sk3)), inference(cnf_transformation, [status(esa)], [f14_sk])).
% 24.69/3.66 cnf(p712, plain, ($false | ~spl27), inference(resolution, [status(thm)], [p710, c17])).
% 24.69/3.66 cnf(sct4, plain, (~spl27), inference(avatar_contradiction_clause, [status(thm)], [p712])).
% 24.69/3.66 fof(sdef37, definition, (spl37 <=> (distinct_points(sk0,sk0))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 24.69/3.66 cnf(p740, plain, (distinct_points(sk0,sk0) | ~spl37), inference(avatar_component_clause, [status(thm)], [sdef37])).
% 24.69/3.66 cnf(p763, plain, ($false | ~spl37), inference(resolution, [status(thm)], [p740, c0])).
% 24.69/3.66 cnf(sct5, plain, (~spl37), inference(avatar_contradiction_clause, [status(thm)], [p763])).
% 24.69/3.66 fof(sdef38, definition, (spl38 <=> (apart_point_and_line(sk3,line_connecting(sk3,sk2)))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 24.69/3.66 cnf(p750, plain, (apart_point_and_line(sk3,line_connecting(sk3,sk2)) | ~spl38), inference(avatar_component_clause, [status(thm)], [sdef38])).
% 24.69/3.66 fof(f3, axiom, ! [X,Y,Z] : ( distinct_points(X,Y) => ( distinct_points(X,Z) | distinct_points(Y,Z) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', apart4)).
% 24.69/3.66 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])).
% 24.69/3.66 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])).
% 24.69/3.66 cnf(c3, plain, ~distinct_points(X0,X1) | distinct_points(X0,X2) | distinct_points(X1,X2), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 24.69/3.66 cnf(c15, plain, distinct_points(sk2,sk3), inference(cnf_transformation, [status(esa)], [f14_sk])).
% 24.69/3.66 cnf(p22, plain, distinct_points(sk2,X0) | distinct_points(sk3,X0), inference(resolution, [status(thm)], [c3, c15])).
% 24.69/3.66 cnf(p24, plain, distinct_points(sk2,X0) | distinct_points(sk3,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p22, c3])).
% 24.69/3.66 cnf(p30, plain, distinct_points(sk2,X0) | distinct_points(X0,sk3), inference(resolution, [status(thm)], [p24, c0])).
% 24.69/3.66 cnf(p34, plain, distinct_points(X0,sk3) | distinct_points(sk2,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p30, c3])).
% 24.69/3.66 cnf(p40, plain, distinct_points(X0,sk3) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [p34, c0])).
% 24.69/3.66 cnf(p43, plain, distinct_points(sk3,sk2), inference(resolution, [status(thm)], [p40, c0])).
% 24.69/3.66 cnf(p68, plain, ~apart_point_and_line(sk3,line_connecting(sk3,sk2)), inference(resolution, [status(thm)], [c6, p43])).
% 24.69/3.66 cnf(p768, plain, ($false | ~spl38), inference(resolution, [status(thm)], [p750, p68])).
% 24.69/3.66 cnf(sct6, plain, (~spl38), inference(avatar_contradiction_clause, [status(thm)], [p768])).
% 24.69/3.66 fof(sdef45, definition, (spl45 <=> (apart_point_and_line(sk1,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 24.69/3.66 cnf(p776, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk1)) | ~spl45), inference(avatar_component_clause, [status(thm)], [sdef45])).
% 24.69/3.66 fof(sdef36, definition, (spl36 <=> (distinct_points(sk2,sk1))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 24.69/3.66 cnf(p739, plain, (distinct_points(sk2,sk1) | ~spl36), inference(avatar_component_clause, [status(thm)], [sdef36])).
% 24.69/3.66 cnf(p761, plain, (~apart_point_and_line(sk1,line_connecting(sk2,sk1)) | ~spl36), inference(resolution, [status(thm)], [p739, c7])).
% 24.69/3.66 cnf(p801, plain, ($false | ~spl36 | ~spl45), inference(resolution, [status(thm)], [p776, p761])).
% 24.69/3.66 cnf(sct7, plain, (~spl36 | ~spl45), inference(avatar_contradiction_clause, [status(thm)], [p801])).
% 24.69/3.66 fof(sdef77, definition, (spl77 <=> (apart_point_and_line(sk1,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl77])], [avatar_definition])).
% 24.69/3.66 cnf(p895, plain, (apart_point_and_line(sk1,line_connecting(sk1,sk2)) | ~spl77), inference(avatar_component_clause, [status(thm)], [sdef77])).
% 24.69/3.66 fof(sdef63, definition, (spl63 <=> (distinct_points(sk1,sk2))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 24.69/3.66 cnf(p833, plain, (distinct_points(sk1,sk2) | ~spl63), inference(avatar_component_clause, [status(thm)], [sdef63])).
% 24.69/3.66 cnf(p850, plain, (~apart_point_and_line(sk1,line_connecting(sk1,sk2)) | ~spl63), inference(resolution, [status(thm)], [p833, c6])).
% 24.69/3.66 cnf(p932, plain, ($false | ~spl63 | ~spl77), inference(resolution, [status(thm)], [p895, p850])).
% 24.69/3.66 cnf(sct8, plain, (~spl63 | ~spl77), inference(avatar_contradiction_clause, [status(thm)], [p932])).
% 24.69/3.66 fof(sdef85, definition, (spl85 <=> (apart_point_and_line(sk2,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl85])], [avatar_definition])).
% 24.69/3.66 cnf(p910, plain, (apart_point_and_line(sk2,line_connecting(sk1,sk2)) | ~spl85), inference(avatar_component_clause, [status(thm)], [sdef85])).
% 24.69/3.66 cnf(p851, plain, (~apart_point_and_line(sk2,line_connecting(sk1,sk2)) | ~spl63), inference(resolution, [status(thm)], [p833, c7])).
% 24.69/3.66 cnf(p947, plain, ($false | ~spl63 | ~spl85), inference(resolution, [status(thm)], [p910, p851])).
% 24.69/3.66 cnf(sct9, plain, (~spl63 | ~spl85), inference(avatar_contradiction_clause, [status(thm)], [p947])).
% 24.69/3.66 fof(sdef28, definition, (spl28 <=> (apart_point_and_line(sk0,line_connecting(sk3,sk2)))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 24.69/3.66 cnf(p715, plain, (apart_point_and_line(sk0,line_connecting(sk3,sk2)) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 24.69/3.66 fof(f11, axiom, ! [X,Y,Z] : ( apart_point_and_line(X,Y) => ( distinct_points(X,Z) | apart_point_and_line(Z,Y) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ceq1)).
% 24.69/3.66 fof(f11_nnf, plain, ! [X,Y,Z] : ((~(apart_point_and_line(X,Y)) | (distinct_points(X,Z) | apart_point_and_line(Z,Y)))), inference(nnf_transformation, [status(thm)], [f11])).
% 24.69/3.66 fof(f11_sk, plain, ! [X,Y,Z] : ((~(apart_point_and_line(X,Y)) | (distinct_points(X,Z) | apart_point_and_line(Z,Y)))), inference(skolemisation, [status(esa)], [f11_nnf])).
% 24.69/3.66 cnf(c11, plain, ~apart_point_and_line(X0,X1) | distinct_points(X0,X2) | apart_point_and_line(X2,X1), inference(cnf_transformation, [status(esa)], [f11_sk])).
% 24.69/3.66 cnf(p717, plain, (distinct_points(sk0,X0) | apart_point_and_line(X0,line_connecting(sk3,sk2)) | ~spl28), inference(resolution, [status(thm)], [p715, c11])).
% 24.69/3.66 cnf(p92, plain, ~apart_point_and_line(sk2,line_connecting(sk3,sk2)), inference(resolution, [status(thm)], [c7, p43])).
% 24.69/3.66 cnf(p1025, plain, (distinct_points(sk0,sk2) | ~spl28), inference(resolution, [status(thm)], [p717, p92])).
% 24.69/3.66 cnf(p1034, plain, (~apart_point_and_line(sk2,line_connecting(sk0,sk2)) | ~spl28), inference(resolution, [status(thm)], [p1025, c7])).
% 24.69/3.66 fof(sdef66, definition, (spl66 <=> (apart_point_and_line(sk2,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 24.69/3.66 cnf(p843, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk2)) | ~spl66), inference(avatar_component_clause, [status(thm)], [sdef66])).
% 24.69/3.66 cnf(p1053, plain, ($false | ~spl28 | ~spl66), inference(resolution, [status(thm)], [p1034, p843])).
% 24.69/3.66 cnf(sct10, plain, (~spl28 | ~spl66), inference(avatar_contradiction_clause, [status(thm)], [p1053])).
% 24.69/3.66 fof(sdef96, definition, (spl96 <=> (apart_point_and_line(sk2,line_connecting(sk3,sk2)))), introduced(definition, [new_symbols(naming, [spl96])], [avatar_definition])).
% 24.69/3.66 cnf(p1108, plain, (apart_point_and_line(sk2,line_connecting(sk3,sk2)) | ~spl96), inference(avatar_component_clause, [status(thm)], [sdef96])).
% 24.69/3.66 cnf(p1132, plain, ($false | ~spl96), inference(resolution, [status(thm)], [p1108, p92])).
% 24.69/3.66 cnf(sct11, plain, (~spl96), inference(avatar_contradiction_clause, [status(thm)], [p1132])).
% 24.69/3.66 fof(sdef110, definition, (spl110 <=> (distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl110])], [avatar_definition])).
% 24.69/3.66 cnf(p1150, plain, (distinct_points(sk0,X0) | ~spl110), inference(avatar_component_clause, [status(thm)], [sdef110])).
% 24.69/3.66 cnf(p1154, plain, ($false | ~spl110), inference(resolution, [status(thm)], [p1150, c0])).
% 24.69/3.66 cnf(sct12, plain, (~spl110), inference(avatar_contradiction_clause, [status(thm)], [p1154])).
% 24.69/3.66 fof(sdef111, definition, (spl111 <=> (distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl111])], [avatar_definition])).
% 24.69/3.66 cnf(p1156, plain, (distinct_points(sk1,X0) | ~spl111), inference(avatar_component_clause, [status(thm)], [sdef111])).
% 24.69/3.66 cnf(p1158, plain, ($false | ~spl111), inference(resolution, [status(thm)], [p1156, c0])).
% 24.69/3.66 cnf(sct13, plain, (~spl111), inference(avatar_contradiction_clause, [status(thm)], [p1158])).
% 24.69/3.66 fof(sdef137, definition, (spl137 <=> (distinct_points(sk0,sk2))), introduced(definition, [new_symbols(naming, [spl137])], [avatar_definition])).
% 24.69/3.66 cnf(p1288, plain, (distinct_points(sk0,sk2) | ~spl137), inference(avatar_component_clause, [status(thm)], [sdef137])).
% 24.69/3.66 cnf(p1306, plain, (~apart_point_and_line(sk2,line_connecting(sk0,sk2)) | ~spl137), inference(resolution, [status(thm)], [p1288, c7])).
% 24.69/3.66 cnf(p1333, plain, ($false | ~spl66 | ~spl137), inference(resolution, [status(thm)], [p1306, p843])).
% 24.69/3.66 cnf(sct14, plain, (~spl66 | ~spl137), inference(avatar_contradiction_clause, [status(thm)], [p1333])).
% 24.69/3.66 fof(sdef139, definition, (spl139 <=> (distinct_points(sk2,sk0))), introduced(definition, [new_symbols(naming, [spl139])], [avatar_definition])).
% 24.69/3.66 cnf(p1292, plain, (distinct_points(sk2,sk0) | ~spl139), inference(avatar_component_clause, [status(thm)], [sdef139])).
% 24.69/3.66 cnf(p1319, plain, (~apart_point_and_line(sk2,line_connecting(sk2,sk0)) | ~spl139), inference(resolution, [status(thm)], [p1292, c6])).
% 24.69/3.66 fof(sdef114, definition, (spl114 <=> (apart_point_and_line(sk2,line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl114])], [avatar_definition])).
% 24.69/3.66 cnf(p1189, plain, (apart_point_and_line(sk2,line_connecting(sk2,sk0)) | ~spl114), inference(avatar_component_clause, [status(thm)], [sdef114])).
% 24.69/3.66 cnf(p1334, plain, ($false | ~spl114 | ~spl139), inference(resolution, [status(thm)], [p1319, p1189])).
% 24.69/3.66 cnf(sct15, plain, (~spl114 | ~spl139), inference(avatar_contradiction_clause, [status(thm)], [p1334])).
% 24.69/3.66 fof(sdef151, definition, (spl151 <=> (apart_point_and_line(sk2,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl151])], [avatar_definition])).
% 24.69/3.66 cnf(p1446, plain, (apart_point_and_line(sk2,line_connecting(sk2,sk1)) | ~spl151), inference(avatar_component_clause, [status(thm)], [sdef151])).
% 24.69/3.66 cnf(p760, plain, (~apart_point_and_line(sk2,line_connecting(sk2,sk1)) | ~spl36), inference(resolution, [status(thm)], [p739, c6])).
% 24.69/3.66 cnf(p1474, plain, ($false | ~spl36 | ~spl151), inference(resolution, [status(thm)], [p1446, p760])).
% 24.69/3.66 cnf(sct16, plain, (~spl36 | ~spl151), inference(avatar_contradiction_clause, [status(thm)], [p1474])).
% 24.69/3.66 fof(sdef160, definition, (spl160 <=> (distinct_points(sk0,X0) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl160])], [avatar_definition])).
% 24.69/3.66 cnf(p1485, plain, (distinct_points(sk0,X0) | distinct_points(sk0,X0) | ~spl160), inference(avatar_component_clause, [status(thm)], [sdef160])).
% 24.69/3.66 cnf(p1526, plain, (distinct_points(sk0,X0) | ~spl160), inference(factoring, [status(thm)], [p1485])).
% 24.69/3.66 cnf(p1527, plain, ($false | ~spl160), inference(resolution, [status(thm)], [p1526, c0])).
% 24.69/3.66 cnf(sct17, plain, (~spl160), inference(avatar_contradiction_clause, [status(thm)], [p1527])).
% 24.69/3.66 fof(sdef163, definition, (spl163 <=> (distinct_points(sk0,X0) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl163])], [avatar_definition])).
% 24.69/3.66 cnf(p1503, plain, (distinct_points(sk0,X0) | distinct_points(X0,sk0) | ~spl163), inference(avatar_component_clause, [status(thm)], [sdef163])).
% 24.69/3.66 cnf(p1546, plain, (distinct_points(sk0,sk0) | ~spl163), inference(factoring, [status(thm)], [p1503])).
% 24.69/3.66 cnf(p1555, plain, ($false | ~spl163), inference(resolution, [status(thm)], [p1546, c0])).
% 24.69/3.66 cnf(sct18, plain, (~spl163), inference(avatar_contradiction_clause, [status(thm)], [p1555])).
% 24.69/3.66 fof(sdef166, definition, (spl166 <=> (distinct_points(sk3,sk3))), introduced(definition, [new_symbols(naming, [spl166])], [avatar_definition])).
% 24.69/3.66 cnf(p1558, plain, (distinct_points(sk3,sk3) | ~spl166), inference(avatar_component_clause, [status(thm)], [sdef166])).
% 24.69/3.66 cnf(p1643, plain, ($false | ~spl166), inference(resolution, [status(thm)], [p1558, c0])).
% 24.69/3.66 cnf(sct19, plain, (~spl166), inference(avatar_contradiction_clause, [status(thm)], [p1643])).
% 24.69/3.66 cnf(c18, plain, apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk3,line_connecting(sk0,sk1)), inference(cnf_transformation, [status(esa)], [f14_sk])).
% 24.69/3.66 fof(sdef0, definition, (spl0 <=> (apart_point_and_line(sk2,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 24.69/3.66 fof(sdef1, definition, (spl1 <=> (apart_point_and_line(sk3,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 24.69/3.66 cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [c18, sdef0, sdef1])).
% 24.69/3.66 cnf(p19, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 24.69/3.66 cnf(p113, plain, (distinct_points(sk2,X0) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | ~spl0), inference(resolution, [status(thm)], [c11, p19])).
% 24.69/3.66 fof(f12, axiom, ! [X,Y,Z] : ( apart_point_and_line(X,Y) => ( distinct_lines(Y,Z) | apart_point_and_line(X,Z) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ceq2)).
% 24.69/3.66 fof(f12_nnf, plain, ! [X,Y,Z] : ((~(apart_point_and_line(X,Y)) | (distinct_lines(Y,Z) | apart_point_and_line(X,Z)))), inference(nnf_transformation, [status(thm)], [f12])).
% 24.69/3.66 fof(f12_sk, plain, ! [X,Y,Z] : ((~(apart_point_and_line(X,Y)) | (distinct_lines(Y,Z) | apart_point_and_line(X,Z)))), inference(skolemisation, [status(esa)], [f12_nnf])).
% 24.69/3.66 cnf(c12, plain, ~apart_point_and_line(X0,X1) | distinct_lines(X1,X2) | apart_point_and_line(X0,X2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 24.69/3.66 cnf(p120, plain, (distinct_points(sk2,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | apart_point_and_line(X0,X1) | ~spl0), inference(resolution, [status(thm)], [p113, c12])).
% 24.69/3.66 cnf(p46, plain, ~apart_point_and_line(sk2,line_connecting(sk2,sk3)), inference(resolution, [status(thm)], [c6, c15])).
% 24.69/3.66 cnf(p646, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk3)) | ~spl0), inference(resolution, [status(thm)], [p120, p46])).
% 24.69/3.66 fof(sdef3, definition, (spl3 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk3)))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 24.69/3.66 cnf(ssp1, plain, (~spl0 | spl2 | spl3), inference(avatar_split_clause, [status(thm)], [p646, sdef2, sdef3])).
% 24.69/3.66 cnf(p649, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk2)) | ~spl0), inference(resolution, [status(thm)], [p120, p92])).
% 24.69/3.66 fof(sdef4, definition, (spl4 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk2)))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 24.69/3.66 cnf(ssp2, plain, (~spl0 | spl2 | spl4), inference(avatar_split_clause, [status(thm)], [p649, sdef2, sdef4])).
% 24.69/3.66 cnf(p57, plain, ~apart_point_and_line(sk2,line_connecting(sk2,X0)) | distinct_points(X0,sk3), inference(resolution, [status(thm)], [c6, p30])).
% 24.69/3.66 cnf(p651, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X0,sk3) | ~spl0), inference(resolution, [status(thm)], [p120, p57])).
% 24.69/3.66 fof(sdef5, definition, (spl5 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X0,sk3))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 24.69/3.66 cnf(ssp3, plain, (~spl0 | spl2 | spl5), inference(avatar_split_clause, [status(thm)], [p651, sdef2, sdef5])).
% 24.69/3.66 cnf(p117, plain, (distinct_points(sk2,sk0) | ~spl0), inference(resolution, [status(thm)], [p113, p45])).
% 24.69/3.66 cnf(p122, plain, (~apart_point_and_line(sk2,line_connecting(sk2,sk0)) | ~spl0), inference(resolution, [status(thm)], [p117, c6])).
% 24.69/3.66 cnf(p657, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk0)) | ~spl0), inference(resolution, [status(thm)], [p120, p122])).
% 24.69/3.66 fof(sdef6, definition, (spl6 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 24.69/3.66 cnf(ssp4, plain, (~spl0 | spl2 | spl6), inference(avatar_split_clause, [status(thm)], [p657, sdef2, sdef6])).
% 24.69/3.66 cnf(p118, plain, (distinct_points(sk2,sk1) | ~spl0), inference(resolution, [status(thm)], [p113, p69])).
% 24.69/3.66 cnf(p126, plain, (~apart_point_and_line(sk2,line_connecting(sk2,sk1)) | ~spl0), inference(resolution, [status(thm)], [p118, c6])).
% 24.69/3.66 cnf(p659, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk1)) | ~spl0), inference(resolution, [status(thm)], [p120, p126])).
% 24.69/3.66 fof(sdef7, definition, (spl7 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 24.69/3.66 cnf(ssp5, plain, (~spl0 | spl2 | spl7), inference(avatar_split_clause, [status(thm)], [p659, sdef2, sdef7])).
% 24.69/3.66 cnf(p121, plain, (distinct_points(sk2,X0) | distinct_points(sk0,X0) | ~spl0), inference(resolution, [status(thm)], [p117, c3])).
% 24.69/3.66 cnf(p129, plain, (distinct_points(sk0,sk2) | ~spl0), inference(resolution, [status(thm)], [p121, c0])).
% 24.69/3.66 cnf(p152, plain, (~apart_point_and_line(sk2,line_connecting(sk0,sk2)) | ~spl0), inference(resolution, [status(thm)], [p129, c7])).
% 24.69/3.66 cnf(p661, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)) | ~spl0), inference(resolution, [status(thm)], [p120, p152])).
% 24.69/3.66 fof(sdef8, definition, (spl8 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 24.69/3.66 cnf(ssp6, plain, (~spl0 | spl2 | spl8), inference(avatar_split_clause, [status(thm)], [p661, sdef2, sdef8])).
% 24.69/3.66 cnf(p125, plain, (distinct_points(sk2,X0) | distinct_points(sk1,X0) | ~spl0), inference(resolution, [status(thm)], [p118, c3])).
% 24.69/3.66 cnf(p153, plain, (distinct_points(sk1,sk2) | ~spl0), inference(resolution, [status(thm)], [p125, c0])).
% 24.69/3.66 cnf(p173, plain, (~apart_point_and_line(sk2,line_connecting(sk1,sk2)) | ~spl0), inference(resolution, [status(thm)], [p153, c7])).
% 24.69/3.66 cnf(p663, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk2)) | ~spl0), inference(resolution, [status(thm)], [p120, p173])).
% 24.69/3.66 fof(sdef9, definition, (spl9 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 24.69/3.66 cnf(ssp7, plain, (~spl0 | spl2 | spl9), inference(avatar_split_clause, [status(thm)], [p663, sdef2, sdef9])).
% 24.69/3.66 cnf(p131, plain, (distinct_points(sk0,X0) | ~apart_point_and_line(sk2,line_connecting(sk2,X0)) | ~spl0), inference(resolution, [status(thm)], [p121, c6])).
% 24.69/3.66 cnf(p665, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk0,X0) | ~spl0), inference(resolution, [status(thm)], [p120, p131])).
% 24.69/3.66 fof(sdef10, definition, (spl10 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 24.69/3.66 cnf(ssp8, plain, (~spl0 | spl2 | spl10), inference(avatar_split_clause, [status(thm)], [p665, sdef2, sdef10])).
% 24.69/3.66 cnf(p155, plain, (distinct_points(sk1,X0) | ~apart_point_and_line(sk2,line_connecting(sk2,X0)) | ~spl0), inference(resolution, [status(thm)], [p125, c6])).
% 24.69/3.66 cnf(p667, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk1,X0) | ~spl0), inference(resolution, [status(thm)], [p120, p155])).
% 24.69/3.66 fof(sdef11, definition, (spl11 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 24.69/3.66 cnf(ssp9, plain, (~spl0 | spl2 | spl11), inference(avatar_split_clause, [status(thm)], [p667, sdef2, sdef11])).
% 24.69/3.66 cnf(p44, plain, distinct_points(X0,sk2) | distinct_points(X0,X1) | distinct_points(sk3,X1), inference(resolution, [status(thm)], [p40, c3])).
% 24.69/3.66 cnf(p316, plain, distinct_points(X0,sk2) | distinct_points(sk3,X0), inference(resolution, [status(thm)], [p44, c0])).
% 24.69/3.66 cnf(p329, plain, distinct_points(sk3,X0) | ~apart_point_and_line(sk2,line_connecting(X0,sk2)), inference(resolution, [status(thm)], [p316, c7])).
% 24.69/3.66 cnf(p669, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(sk3,X0) | ~spl0), inference(resolution, [status(thm)], [p120, p329])).
% 24.69/3.66 fof(sdef12, definition, (spl12 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(sk3,X0))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 24.69/3.66 cnf(ssp10, plain, (~spl0 | spl2 | spl12), inference(avatar_split_clause, [status(thm)], [p669, sdef2, sdef12])).
% 24.69/3.66 cnf(p130, plain, (distinct_points(sk0,X0) | distinct_points(sk2,X1) | distinct_points(X0,X1) | ~spl0), inference(resolution, [status(thm)], [p121, c3])).
% 24.69/3.66 cnf(p343, plain, (distinct_points(sk0,X0) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p130, c0])).
% 24.69/3.66 cnf(p360, plain, (distinct_points(sk0,X0) | ~apart_point_and_line(sk2,line_connecting(X0,sk2)) | ~spl0), inference(resolution, [status(thm)], [p343, c7])).
% 24.69/3.66 cnf(p673, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(sk0,X0) | ~spl0), inference(resolution, [status(thm)], [p120, p360])).
% 24.69/3.66 fof(sdef13, definition, (spl13 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 24.69/3.66 cnf(ssp11, plain, (~spl0 | spl2 | spl13), inference(avatar_split_clause, [status(thm)], [p673, sdef2, sdef13])).
% 24.69/3.66 cnf(p154, plain, (distinct_points(sk1,X0) | distinct_points(sk2,X1) | distinct_points(X0,X1) | ~spl0), inference(resolution, [status(thm)], [p125, c3])).
% 24.69/3.66 cnf(p370, plain, (distinct_points(sk1,X0) | distinct_points(X0,sk2) | ~spl0), inference(resolution, [status(thm)], [p154, c0])).
% 24.69/3.66 cnf(p387, plain, (distinct_points(sk1,X0) | ~apart_point_and_line(sk2,line_connecting(X0,sk2)) | ~spl0), inference(resolution, [status(thm)], [p370, c7])).
% 24.69/3.66 cnf(p676, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(sk1,X0) | ~spl0), inference(resolution, [status(thm)], [p120, p387])).
% 24.69/3.66 fof(sdef14, definition, (spl14 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 24.69/3.66 cnf(ssp12, plain, (~spl0 | spl2 | spl14), inference(avatar_split_clause, [status(thm)], [p676, sdef2, sdef14])).
% 24.69/3.66 cnf(p54, plain, ~apart_point_and_line(sk2,line_connecting(sk2,X0)) | distinct_points(sk3,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [c6, p24])).
% 24.69/3.66 cnf(p678, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk3,X1) | distinct_points(X0,X1) | ~spl0), inference(resolution, [status(thm)], [p120, p54])).
% 24.69/3.66 fof(sdef15, definition, (spl15 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(sk3,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 24.69/3.66 cnf(ssp13, plain, (~spl0 | spl2 | spl15), inference(avatar_split_clause, [status(thm)], [p678, sdef2, sdef15])).
% 24.69/3.66 cnf(p356, plain, (distinct_points(X0,sk2) | distinct_points(sk0,X1) | distinct_points(X0,X1) | ~spl0), inference(resolution, [status(thm)], [p343, c3])).
% 24.69/3.66 cnf(p471, plain, (distinct_points(X0,sk2) | distinct_points(X0,sk0) | ~spl0), inference(resolution, [status(thm)], [p356, c0])).
% 24.69/3.66 cnf(p485, plain, (distinct_points(X0,sk0) | ~apart_point_and_line(sk2,line_connecting(X0,sk2)) | ~spl0), inference(resolution, [status(thm)], [p471, c7])).
% 24.69/3.66 cnf(p681, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(X0,sk0) | ~spl0), inference(resolution, [status(thm)], [p120, p485])).
% 24.69/3.66 fof(sdef16, definition, (spl16 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 24.69/3.66 cnf(ssp14, plain, (~spl0 | spl2 | spl16), inference(avatar_split_clause, [status(thm)], [p681, sdef2, sdef16])).
% 24.69/3.66 cnf(p383, plain, (distinct_points(X0,sk2) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl0), inference(resolution, [status(thm)], [p370, c3])).
% 24.69/3.66 cnf(p487, plain, (distinct_points(X0,sk2) | distinct_points(X0,sk1) | ~spl0), inference(resolution, [status(thm)], [p383, c0])).
% 24.69/3.66 cnf(p501, plain, (distinct_points(X0,sk1) | ~apart_point_and_line(sk2,line_connecting(X0,sk2)) | ~spl0), inference(resolution, [status(thm)], [p487, c7])).
% 24.69/3.66 cnf(p684, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(X0,sk1) | ~spl0), inference(resolution, [status(thm)], [p120, p501])).
% 24.69/3.66 fof(sdef17, definition, (spl17 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk2)) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 24.69/3.66 cnf(ssp15, plain, (~spl0 | spl2 | spl17), inference(avatar_split_clause, [status(thm)], [p684, sdef2, sdef17])).
% 24.69/3.66 cnf(p65, plain, ~apart_point_and_line(sk2,line_connecting(sk2,X0)) | distinct_points(X1,sk3) | distinct_points(X1,X0), inference(resolution, [status(thm)], [c6, p34])).
% 24.69/3.66 cnf(p686, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X1,sk3) | distinct_points(X1,X0) | ~spl0), inference(resolution, [status(thm)], [p120, p65])).
% 24.69/3.66 fof(sdef18, definition, (spl18 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X1,sk3) | distinct_points(X1,X0))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 24.69/3.66 cnf(ssp16, plain, (~spl0 | spl2 | spl18), inference(avatar_split_clause, [status(thm)], [p686, sdef2, sdef18])).
% 24.69/3.66 cnf(p483, plain, (distinct_points(X0,sk0) | distinct_points(X0,X1) | distinct_points(sk2,X1) | ~spl0), inference(resolution, [status(thm)], [p471, c3])).
% 24.69/3.66 cnf(p535, plain, (distinct_points(X0,sk0) | distinct_points(sk2,X0) | ~spl0), inference(resolution, [status(thm)], [p483, c0])).
% 24.69/3.66 cnf(p548, plain, (distinct_points(X0,sk0) | ~apart_point_and_line(sk2,line_connecting(sk2,X0)) | ~spl0), inference(resolution, [status(thm)], [p535, c6])).
% 24.69/3.66 cnf(p689, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X0,sk0) | ~spl0), inference(resolution, [status(thm)], [p120, p548])).
% 24.69/3.66 fof(sdef19, definition, (spl19 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 24.69/3.66 cnf(ssp17, plain, (~spl0 | spl2 | spl19), inference(avatar_split_clause, [status(thm)], [p689, sdef2, sdef19])).
% 24.69/3.66 cnf(p499, plain, (distinct_points(X0,sk1) | distinct_points(X0,X1) | distinct_points(sk2,X1) | ~spl0), inference(resolution, [status(thm)], [p487, c3])).
% 24.69/3.66 cnf(p552, plain, (distinct_points(X0,sk1) | distinct_points(sk2,X0) | ~spl0), inference(resolution, [status(thm)], [p499, c0])).
% 24.69/3.66 cnf(p565, plain, (distinct_points(X0,sk1) | ~apart_point_and_line(sk2,line_connecting(sk2,X0)) | ~spl0), inference(resolution, [status(thm)], [p552, c6])).
% 24.69/3.66 cnf(p692, plain, (distinct_points(sk2,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X0,sk1) | ~spl0), inference(resolution, [status(thm)], [p120, p565])).
% 24.69/3.66 fof(sdef20, definition, (spl20 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,X0)) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 24.69/3.66 cnf(ssp18, plain, (~spl0 | spl2 | spl20), inference(avatar_split_clause, [status(thm)], [p692, sdef2, sdef20])).
% 24.69/3.66 fof(f10, axiom, ! [X,Y,U,V] : ( ( distinct_points(X,Y) & distinct_lines(U,V) ) => ( apart_point_and_line(X,U) | apart_point_and_line(X,V) | apart_point_and_line(Y,U) | apart_point_and_line(Y,V) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cu1)).
% 24.69/3.66 fof(f10_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)], [f10])).
% 24.69/3.66 fof(f10_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)], [f10_nnf])).
% 24.69/3.66 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)], [f10_sk])).
% 24.69/3.66 cnf(p93, 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])).
% 24.69/3.66 cnf(p115, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | apart_point_and_line(sk2,X0) | ~spl0), inference(resolution, [status(thm)], [c12, p19])).
% 24.69/3.66 cnf(p697, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | ~spl0), inference(resolution, [status(thm)], [p93, p115])).
% 24.69/3.66 fof(sdef22, definition, (spl22 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 24.69/3.66 cnf(ssp19, plain, (~spl0 | spl21 | spl22 | spl23), inference(avatar_split_clause, [status(thm)], [p697, sdef21, sdef22, sdef23])).
% 24.69/3.66 cnf(p20, plain, (apart_point_and_line(sk3,line_connecting(sk0,sk1)) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 24.69/3.66 cnf(p116, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | apart_point_and_line(sk3,X0) | ~spl1), inference(resolution, [status(thm)], [c12, p20])).
% 24.69/3.66 cnf(p701, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk3,X0) | ~spl1), inference(resolution, [status(thm)], [p93, p116])).
% 24.69/3.66 fof(sdef24, definition, (spl24 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk3,X0))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 24.69/3.66 cnf(ssp20, plain, (~spl1 | spl21 | spl23 | spl24), inference(avatar_split_clause, [status(thm)], [p701, sdef21, sdef23, sdef24])).
% 24.69/3.66 cnf(p703, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | distinct_points(sk2,X1) | apart_point_and_line(X1,X0) | ~spl0), inference(resolution, [status(thm)], [p93, p120])).
% 24.69/3.66 fof(sdef25, definition, (spl25 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_points(sk2,X1) | apart_point_and_line(X1,X0))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 24.69/3.66 cnf(ssp21, plain, (~spl0 | spl21 | spl23 | spl25), inference(avatar_split_clause, [status(thm)], [p703, sdef21, sdef23, sdef25])).
% 24.69/3.66 cnf(p648, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk3)) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 24.69/3.66 cnf(p708, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk3)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk3)) | ~spl3), inference(resolution, [status(thm)], [p648, p93])).
% 24.69/3.66 cnf(ssp22, plain, (~spl3 | spl21 | spl23 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p708, sdef21, sdef23, sdef26, sdef27])).
% 24.69/3.66 cnf(p650, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk2)) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 24.69/3.66 cnf(p714, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk3,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk3,sk2)) | ~spl4), inference(resolution, [status(thm)], [p650, p93])).
% 24.69/3.66 fof(sdef29, definition, (spl29 <=> (apart_point_and_line(sk1,line_connecting(sk3,sk2)))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 24.69/3.66 cnf(ssp23, plain, (~spl4 | spl21 | spl23 | spl28 | spl29), inference(avatar_split_clause, [status(thm)], [p714, sdef21, sdef23, sdef28, sdef29])).
% 24.69/3.66 cnf(p21, plain, distinct_points(sk0,X0) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [c3, c14])).
% 24.69/3.66 cnf(p95, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(sk0,X2), inference(resolution, [status(thm)], [c10, p21])).
% 24.69/3.66 cnf(p721, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | apart_point_and_line(sk3,X0) | ~spl1), inference(resolution, [status(thm)], [p95, p116])).
% 24.69/3.66 fof(sdef30, definition, (spl30 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | apart_point_and_line(sk3,X0))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 24.69/3.66 cnf(ssp24, plain, (~spl1 | spl23 | spl30), inference(avatar_split_clause, [status(thm)], [p721, sdef23, sdef30])).
% 24.69/3.66 cnf(p723, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk3,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk3,sk2)) | distinct_points(sk0,X0) | ~spl4), inference(resolution, [status(thm)], [p95, p650])).
% 24.69/3.66 fof(sdef31, definition, (spl31 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk3,sk2)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 24.69/3.66 cnf(ssp25, plain, (~spl4 | spl23 | spl29 | spl31), inference(avatar_split_clause, [status(thm)], [p723, sdef23, sdef29, sdef31])).
% 24.69/3.66 cnf(p658, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk0)) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 24.69/3.66 cnf(p726, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | ~spl6), inference(resolution, [status(thm)], [p658, p93])).
% 24.69/3.66 fof(sdef32, definition, (spl32 <=> (apart_point_and_line(sk0,line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 24.69/3.66 fof(sdef33, definition, (spl33 <=> (apart_point_and_line(sk1,line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 24.69/3.66 cnf(ssp26, plain, (~spl6 | spl21 | spl23 | spl32 | spl33), inference(avatar_split_clause, [status(thm)], [p726, sdef21, sdef23, sdef32, sdef33])).
% 24.69/3.66 cnf(p729, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(sk0,X0) | ~spl6), inference(resolution, [status(thm)], [p658, p95])).
% 24.69/3.66 fof(sdef34, definition, (spl34 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 24.69/3.66 cnf(ssp27, plain, (~spl6 | spl23 | spl33 | spl34), inference(avatar_split_clause, [status(thm)], [p729, sdef23, sdef33, sdef34])).
% 24.69/3.66 cnf(p727, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk0)) | ~spl32), inference(avatar_component_clause, [status(thm)], [sdef32])).
% 24.69/3.66 cnf(p80, plain, ~apart_point_and_line(X0,line_connecting(X1,X0)) | distinct_points(sk2,X1) | distinct_points(sk3,X0), inference(resolution, [status(thm)], [c7, p24])).
% 24.69/3.66 cnf(p736, plain, (distinct_points(sk2,sk2) | distinct_points(sk3,sk0) | ~spl32), inference(resolution, [status(thm)], [p727, p80])).
% 24.69/3.66 fof(sdef35, definition, (spl35 <=> (distinct_points(sk3,sk0))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 24.69/3.66 cnf(ssp28, plain, (~spl32 | spl2 | spl35), inference(avatar_split_clause, [status(thm)], [p736, sdef2, sdef35])).
% 24.69/3.66 cnf(p23, plain, distinct_points(sk0,X0) | distinct_points(sk1,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p21, c3])).
% 24.69/3.66 cnf(p25, plain, distinct_points(sk0,X0) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [p23, c0])).
% 24.69/3.66 cnf(p29, plain, distinct_points(X0,sk1) | distinct_points(sk0,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [p25, c3])).
% 24.69/3.66 cnf(p85, plain, ~apart_point_and_line(X0,line_connecting(X1,X0)) | distinct_points(X1,sk1) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [c7, p29])).
% 24.69/3.66 cnf(p738, plain, (distinct_points(sk2,sk1) | distinct_points(sk0,sk0) | ~spl32), inference(resolution, [status(thm)], [p727, p85])).
% 24.69/3.66 cnf(ssp29, plain, (~spl32 | spl36 | spl37), inference(avatar_split_clause, [status(thm)], [p738, sdef36, sdef37])).
% 24.69/3.66 cnf(p96, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk3,X0) | apart_point_and_line(sk3,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(sk2,X2), inference(resolution, [status(thm)], [c10, p22])).
% 24.69/3.66 cnf(p749, plain, (apart_point_and_line(sk3,line_connecting(sk0,sk1)) | apart_point_and_line(sk3,line_connecting(sk3,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk3,sk2)) | distinct_points(sk2,X0) | ~spl4), inference(resolution, [status(thm)], [p96, p650])).
% 24.69/3.66 fof(sdef39, definition, (spl39 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk3,sk2)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 24.69/3.66 cnf(ssp30, plain, (~spl4 | spl1 | spl38 | spl39), inference(avatar_split_clause, [status(thm)], [p749, sdef1, sdef38, sdef39])).
% 24.69/3.66 cnf(p752, plain, (apart_point_and_line(sk3,line_connecting(sk0,sk1)) | apart_point_and_line(sk3,line_connecting(sk2,sk0)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(sk2,X0) | ~spl6), inference(resolution, [status(thm)], [p96, p658])).
% 24.69/3.66 fof(sdef40, definition, (spl40 <=> (apart_point_and_line(sk3,line_connecting(sk2,sk0)))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 24.69/3.66 fof(sdef41, definition, (spl41 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk0)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 24.69/3.66 cnf(ssp31, plain, (~spl6 | spl1 | spl40 | spl41), inference(avatar_split_clause, [status(thm)], [p752, sdef1, sdef40, sdef41])).
% 24.69/3.66 cnf(p97, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(sk1,X3) | distinct_points(X2,X3), inference(resolution, [status(thm)], [c10, p23])).
% 24.69/3.66 cnf(p766, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | apart_point_and_line(sk3,X0) | ~spl1), inference(resolution, [status(thm)], [p97, p116])).
% 24.69/3.66 fof(sdef42, definition, (spl42 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | apart_point_and_line(sk3,X0))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 24.69/3.66 cnf(ssp32, plain, (~spl1 | spl21 | spl42), inference(avatar_split_clause, [status(thm)], [p766, sdef21, sdef42])).
% 24.69/3.66 cnf(p98, 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,X3) | distinct_points(X3,X2), inference(resolution, [status(thm)], [c10, p23])).
% 24.69/3.66 cnf(p771, 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,X2) | distinct_points(X2,X1) | apart_point_and_line(sk3,X0) | ~spl1), inference(resolution, [status(thm)], [p98, p116])).
% 24.69/3.66 fof(sdef43, definition, (spl43 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X2) | distinct_points(X2,X1) | apart_point_and_line(sk3,X0))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 24.69/3.66 cnf(ssp33, plain, (~spl1 | spl23 | spl43), inference(avatar_split_clause, [status(thm)], [p771, sdef23, sdef43])).
% 24.69/3.66 cnf(p660, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk1)) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 24.69/3.66 cnf(p774, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | ~spl7), inference(resolution, [status(thm)], [p660, p93])).
% 24.69/3.66 fof(sdef44, definition, (spl44 <=> (apart_point_and_line(sk0,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 24.69/3.66 cnf(ssp34, plain, (~spl7 | spl21 | spl23 | spl44 | spl45), inference(avatar_split_clause, [status(thm)], [p774, sdef21, sdef23, sdef44, sdef45])).
% 24.69/3.66 cnf(p777, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk0,X0) | ~spl7), inference(resolution, [status(thm)], [p660, p95])).
% 24.69/3.66 fof(sdef46, definition, (spl46 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 24.69/3.66 cnf(ssp35, plain, (~spl7 | spl23 | spl45 | spl46), inference(avatar_split_clause, [status(thm)], [p777, sdef23, sdef45, sdef46])).
% 24.69/3.66 cnf(p779, plain, (apart_point_and_line(sk3,line_connecting(sk0,sk1)) | apart_point_and_line(sk3,line_connecting(sk2,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk2,X0) | ~spl7), inference(resolution, [status(thm)], [p660, p96])).
% 24.69/3.66 fof(sdef47, definition, (spl47 <=> (apart_point_and_line(sk3,line_connecting(sk2,sk1)))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 24.69/3.66 fof(sdef48, definition, (spl48 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 24.69/3.66 cnf(ssp36, plain, (~spl7 | spl1 | spl47 | spl48), inference(avatar_split_clause, [status(thm)], [p779, sdef1, sdef47, sdef48])).
% 24.69/3.66 cnf(p782, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl7), inference(resolution, [status(thm)], [p660, p97])).
% 24.69/3.66 fof(sdef49, definition, (spl49 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk1,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 24.69/3.66 cnf(ssp37, plain, (~spl7 | spl21 | spl44 | spl49), inference(avatar_split_clause, [status(thm)], [p782, sdef21, sdef44, sdef49])).
% 24.69/3.66 cnf(p784, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk0,X1) | distinct_points(X1,X0) | ~spl7), inference(resolution, [status(thm)], [p660, p98])).
% 24.69/3.66 fof(sdef50, definition, (spl50 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk0,X1) | distinct_points(X1,X0))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 24.69/3.66 cnf(ssp38, plain, (~spl7 | spl23 | spl45 | spl50), inference(avatar_split_clause, [status(thm)], [p784, sdef23, sdef45, sdef50])).
% 24.69/3.66 cnf(p99, plain, ~distinct_lines(X0,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | apart_point_and_line(X3,X0) | apart_point_and_line(X3,X1) | distinct_points(sk0,X2) | distinct_points(sk1,X3), inference(resolution, [status(thm)], [c10, p23])).
% 24.69/3.66 cnf(p789, plain, (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | distinct_points(sk0,X0) | distinct_points(sk1,X1) | ~spl7), inference(resolution, [status(thm)], [p99, p660])).
% 24.69/3.66 fof(sdef51, definition, (spl51 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 24.69/3.66 cnf(ssp39, plain, (~spl7 | spl46 | spl51), inference(avatar_split_clause, [status(thm)], [p789, sdef46, sdef51])).
% 24.69/3.66 cnf(p797, plain, (distinct_points(sk2,sk2) | distinct_points(sk3,sk1) | ~spl45), inference(resolution, [status(thm)], [p776, p80])).
% 24.69/3.66 fof(sdef52, definition, (spl52 <=> (distinct_points(sk3,sk1))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 24.69/3.66 cnf(ssp40, plain, (~spl45 | spl2 | spl52), inference(avatar_split_clause, [status(thm)], [p797, sdef2, sdef52])).
% 24.69/3.66 cnf(p100, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(X2,sk1), inference(resolution, [status(thm)], [c10, p25])).
% 24.69/3.66 cnf(p808, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk1) | apart_point_and_line(sk3,X0) | ~spl1), inference(resolution, [status(thm)], [p100, p116])).
% 24.69/3.66 fof(sdef53, definition, (spl53 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk1) | apart_point_and_line(sk3,X0))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 24.69/3.66 cnf(ssp41, plain, (~spl1 | spl21 | spl53), inference(avatar_split_clause, [status(thm)], [p808, sdef21, sdef53])).
% 24.69/3.66 cnf(p662, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 24.69/3.66 cnf(p811, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | ~spl8), inference(resolution, [status(thm)], [p662, p93])).
% 24.69/3.66 fof(sdef54, definition, (spl54 <=> (apart_point_and_line(sk0,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 24.69/3.66 fof(sdef55, definition, (spl55 <=> (apart_point_and_line(sk1,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 24.69/3.66 cnf(ssp42, plain, (~spl8 | spl21 | spl23 | spl54 | spl55), inference(avatar_split_clause, [status(thm)], [p811, sdef21, sdef23, sdef54, sdef55])).
% 24.69/3.66 cnf(p814, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk0,X0) | ~spl8), inference(resolution, [status(thm)], [p662, p95])).
% 24.69/3.66 fof(sdef56, definition, (spl56 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 24.69/3.66 cnf(ssp43, plain, (~spl8 | spl23 | spl55 | spl56), inference(avatar_split_clause, [status(thm)], [p814, sdef23, sdef55, sdef56])).
% 24.69/3.66 cnf(p816, plain, (apart_point_and_line(sk3,line_connecting(sk0,sk1)) | apart_point_and_line(sk3,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk2,X0) | ~spl8), inference(resolution, [status(thm)], [p662, p96])).
% 24.69/3.66 fof(sdef57, definition, (spl57 <=> (apart_point_and_line(sk3,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 24.69/3.66 fof(sdef58, definition, (spl58 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 24.69/3.66 cnf(ssp44, plain, (~spl8 | spl1 | spl57 | spl58), inference(avatar_split_clause, [status(thm)], [p816, sdef1, sdef57, sdef58])).
% 24.69/3.66 cnf(p819, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl8), inference(resolution, [status(thm)], [p662, p97])).
% 24.69/3.66 fof(sdef59, definition, (spl59 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk1,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 24.69/3.66 cnf(ssp45, plain, (~spl8 | spl21 | spl54 | spl59), inference(avatar_split_clause, [status(thm)], [p819, sdef21, sdef54, sdef59])).
% 24.69/3.66 cnf(p821, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_points(X1,X0) | ~spl8), inference(resolution, [status(thm)], [p662, p98])).
% 24.69/3.66 fof(sdef60, definition, (spl60 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_points(X1,X0))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 24.69/3.66 cnf(ssp46, plain, (~spl8 | spl23 | spl55 | spl60), inference(avatar_split_clause, [status(thm)], [p821, sdef23, sdef55, sdef60])).
% 24.69/3.66 cnf(p823, plain, (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk0,X0) | distinct_points(sk1,X1) | ~spl8), inference(resolution, [status(thm)], [p662, p99])).
% 24.69/3.66 fof(sdef61, definition, (spl61 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 24.69/3.66 cnf(ssp47, plain, (~spl8 | spl56 | spl61), inference(avatar_split_clause, [status(thm)], [p823, sdef56, sdef61])).
% 24.69/3.66 cnf(p825, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X0,sk1) | ~spl8), inference(resolution, [status(thm)], [p662, p100])).
% 24.69/3.66 fof(sdef62, definition, (spl62 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 24.69/3.66 cnf(ssp48, plain, (~spl8 | spl21 | spl54 | spl62), inference(avatar_split_clause, [status(thm)], [p825, sdef21, sdef54, sdef62])).
% 24.69/3.66 cnf(p812, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | ~spl54), inference(avatar_component_clause, [status(thm)], [sdef54])).
% 24.69/3.66 cnf(p51, plain, ~apart_point_and_line(X0,line_connecting(X0,X1)) | distinct_points(sk0,X0) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [c6, p23])).
% 24.69/3.66 cnf(p832, plain, (distinct_points(sk0,sk0) | distinct_points(sk1,sk2) | ~spl54), inference(resolution, [status(thm)], [p812, p51])).
% 24.69/3.66 cnf(ssp49, plain, (~spl54 | spl37 | spl63), inference(avatar_split_clause, [status(thm)], [p832, sdef37, sdef63])).
% 24.69/3.66 cnf(p66, plain, ~apart_point_and_line(X0,line_connecting(X0,X1)) | distinct_points(X0,sk3) | distinct_points(sk2,X1), inference(resolution, [status(thm)], [c6, p34])).
% 24.69/3.66 cnf(p835, plain, (distinct_points(sk0,sk3) | distinct_points(sk2,sk2) | ~spl54), inference(resolution, [status(thm)], [p812, p66])).
% 24.69/3.66 fof(sdef64, definition, (spl64 <=> (distinct_points(sk0,sk3))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 24.69/3.66 cnf(ssp50, plain, (~spl54 | spl2 | spl64), inference(avatar_split_clause, [status(thm)], [p835, sdef2, sdef64])).
% 24.69/3.66 cnf(p101, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(sk3,X3) | distinct_points(X2,X3), inference(resolution, [status(thm)], [c10, p24])).
% 24.69/3.66 cnf(p840, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk3,X2) | distinct_points(X1,X2) | apart_point_and_line(sk3,X0) | ~spl1), inference(resolution, [status(thm)], [p101, p116])).
% 24.69/3.66 fof(sdef65, definition, (spl65 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk3,X2) | distinct_points(X1,X2) | apart_point_and_line(sk3,X0))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 24.69/3.66 cnf(ssp51, plain, (~spl1 | spl0 | spl65), inference(avatar_split_clause, [status(thm)], [p840, sdef0, sdef65])).
% 24.69/3.66 cnf(p842, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk3,X1) | distinct_points(X0,X1) | ~spl8), inference(resolution, [status(thm)], [p101, p662])).
% 24.69/3.66 fof(sdef67, definition, (spl67 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk3,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 24.69/3.66 cnf(ssp52, plain, (~spl8 | spl0 | spl66 | spl67), inference(avatar_split_clause, [status(thm)], [p842, sdef0, sdef66, sdef67])).
% 24.69/3.66 cnf(p102, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk3,X0) | apart_point_and_line(sk3,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(sk2,X3) | distinct_points(X3,X2), inference(resolution, [status(thm)], [c10, p24])).
% 24.69/3.66 cnf(p859, plain, (apart_point_and_line(sk3,line_connecting(sk0,sk1)) | apart_point_and_line(sk3,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk2,X1) | distinct_points(X1,X0) | ~spl8), inference(resolution, [status(thm)], [p102, p662])).
% 24.69/3.66 fof(sdef68, definition, (spl68 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk2,X1) | distinct_points(X1,X0))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 24.69/3.66 cnf(ssp53, plain, (~spl8 | spl1 | spl57 | spl68), inference(avatar_split_clause, [status(thm)], [p859, sdef1, sdef57, sdef68])).
% 24.69/3.66 cnf(p75, plain, ~apart_point_and_line(X0,line_connecting(X1,X0)) | distinct_points(sk0,X1) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [c7, p23])).
% 24.69/3.66 cnf(p868, plain, (distinct_points(sk0,sk0) | distinct_points(sk1,sk2) | ~spl66), inference(resolution, [status(thm)], [p843, p75])).
% 24.69/3.66 cnf(ssp54, plain, (~spl66 | spl37 | spl63), inference(avatar_split_clause, [status(thm)], [p868, sdef37, sdef63])).
% 24.69/3.66 cnf(p90, plain, ~apart_point_and_line(X0,line_connecting(X1,X0)) | distinct_points(X1,sk3) | distinct_points(sk2,X0), inference(resolution, [status(thm)], [c7, p34])).
% 24.69/3.66 cnf(p870, plain, (distinct_points(sk0,sk3) | distinct_points(sk2,sk2) | ~spl66), inference(resolution, [status(thm)], [p843, p90])).
% 24.69/3.66 cnf(ssp55, plain, (~spl66 | spl2 | spl64), inference(avatar_split_clause, [status(thm)], [p870, sdef2, sdef64])).
% 24.69/3.66 cnf(p103, plain, ~distinct_lines(X0,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | apart_point_and_line(X3,X0) | apart_point_and_line(X3,X1) | distinct_points(sk2,X2) | distinct_points(sk3,X3), inference(resolution, [status(thm)], [c10, p24])).
% 24.69/3.66 cnf(p871, plain, (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk2,X0) | distinct_points(sk3,X1) | ~spl8), inference(resolution, [status(thm)], [p103, p662])).
% 24.69/3.66 fof(sdef69, definition, (spl69 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk3,X0))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 24.69/3.66 cnf(ssp56, plain, (~spl8 | spl58 | spl69), inference(avatar_split_clause, [status(thm)], [p871, sdef58, sdef69])).
% 24.69/3.66 cnf(p104, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(X2,sk3), inference(resolution, [status(thm)], [c10, p30])).
% 24.69/3.66 cnf(p880, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk3) | apart_point_and_line(sk3,X0) | ~spl1), inference(resolution, [status(thm)], [p104, p116])).
% 24.69/3.66 fof(sdef70, definition, (spl70 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk3) | apart_point_and_line(sk3,X0))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 24.69/3.66 cnf(ssp57, plain, (~spl1 | spl0 | spl70), inference(avatar_split_clause, [status(thm)], [p880, sdef0, sdef70])).
% 24.69/3.66 cnf(p882, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X0,sk3) | ~spl8), inference(resolution, [status(thm)], [p104, p662])).
% 24.69/3.66 fof(sdef71, definition, (spl71 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X0,sk3))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 24.69/3.66 cnf(ssp58, plain, (~spl8 | spl0 | spl66 | spl71), inference(avatar_split_clause, [status(thm)], [p882, sdef0, sdef66, sdef71])).
% 24.69/3.66 cnf(p105, plain, ~distinct_lines(X0,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_points(sk0,X3) | distinct_points(X2,X3), inference(resolution, [status(thm)], [c10, p29])).
% 24.69/3.66 cnf(p884, plain, (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,X1) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X1) | distinct_points(sk0,X2) | distinct_points(X0,X2) | apart_point_and_line(sk3,X1) | ~spl1), inference(resolution, [status(thm)], [p105, p116])).
% 24.69/3.66 fof(sdef72, definition, (spl72 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,X1) | apart_point_and_line(sk1,X1) | distinct_points(sk0,X2) | distinct_points(X0,X2) | apart_point_and_line(sk3,X1))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 24.69/3.66 cnf(ssp59, plain, (~spl1 | spl23 | spl72), inference(avatar_split_clause, [status(thm)], [p884, sdef23, sdef72])).
% 24.69/3.66 cnf(p886, plain, (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_points(X0,X1) | ~spl8), inference(resolution, [status(thm)], [p105, p662])).
% 24.69/3.66 fof(sdef73, definition, (spl73 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 24.69/3.66 cnf(ssp60, plain, (~spl8 | spl23 | spl55 | spl73), inference(avatar_split_clause, [status(thm)], [p886, sdef23, sdef55, sdef73])).
% 24.69/3.66 cnf(p106, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(X3,sk1) | distinct_points(X3,X2), inference(resolution, [status(thm)], [c10, p29])).
% 24.69/3.66 cnf(p888, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk1) | distinct_points(X2,X1) | apart_point_and_line(sk3,X0) | ~spl1), inference(resolution, [status(thm)], [p106, p116])).
% 24.69/3.66 fof(sdef74, definition, (spl74 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk1) | distinct_points(X2,X1) | apart_point_and_line(sk3,X0))), introduced(definition, [new_symbols(naming, [spl74])], [avatar_definition])).
% 24.69/3.66 cnf(ssp61, plain, (~spl1 | spl21 | spl74), inference(avatar_split_clause, [status(thm)], [p888, sdef21, sdef74])).
% 24.69/3.66 cnf(p890, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X1,sk1) | distinct_points(X1,X0) | ~spl8), inference(resolution, [status(thm)], [p106, p662])).
% 24.69/3.66 fof(sdef75, definition, (spl75 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X1,sk1) | distinct_points(X1,X0))), introduced(definition, [new_symbols(naming, [spl75])], [avatar_definition])).
% 24.69/3.66 cnf(ssp62, plain, (~spl8 | spl21 | spl54 | spl75), inference(avatar_split_clause, [status(thm)], [p890, sdef21, sdef54, sdef75])).
% 24.69/3.66 cnf(p664, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk2)) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 24.69/3.66 cnf(p893, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk1,sk2)) | ~spl9), inference(resolution, [status(thm)], [p664, p93])).
% 24.69/3.66 fof(sdef76, definition, (spl76 <=> (apart_point_and_line(sk0,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl76])], [avatar_definition])).
% 24.69/3.66 cnf(ssp63, plain, (~spl9 | spl21 | spl23 | spl76 | spl77), inference(avatar_split_clause, [status(thm)], [p893, sdef21, sdef23, sdef76, sdef77])).
% 24.69/3.66 cnf(p896, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk0,X0) | ~spl9), inference(resolution, [status(thm)], [p664, p95])).
% 24.69/3.66 fof(sdef78, definition, (spl78 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl78])], [avatar_definition])).
% 24.69/3.66 cnf(ssp64, plain, (~spl9 | spl23 | spl77 | spl78), inference(avatar_split_clause, [status(thm)], [p896, sdef23, sdef77, sdef78])).
% 24.69/3.66 cnf(p898, plain, (apart_point_and_line(sk3,line_connecting(sk0,sk1)) | apart_point_and_line(sk3,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk2,X0) | ~spl9), inference(resolution, [status(thm)], [p664, p96])).
% 24.69/3.66 fof(sdef79, definition, (spl79 <=> (apart_point_and_line(sk3,line_connecting(sk1,sk2)))), introduced(definition, [new_symbols(naming, [spl79])], [avatar_definition])).
% 24.69/3.66 fof(sdef80, definition, (spl80 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl80])], [avatar_definition])).
% 24.69/3.66 cnf(ssp65, plain, (~spl9 | spl1 | spl79 | spl80), inference(avatar_split_clause, [status(thm)], [p898, sdef1, sdef79, sdef80])).
% 24.69/3.66 cnf(p901, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl9), inference(resolution, [status(thm)], [p664, p97])).
% 24.69/3.66 fof(sdef81, definition, (spl81 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk1,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl81])], [avatar_definition])).
% 24.69/3.66 cnf(ssp66, plain, (~spl9 | spl21 | spl76 | spl81), inference(avatar_split_clause, [status(thm)], [p901, sdef21, sdef76, sdef81])).
% 24.69/3.66 cnf(p903, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk0,X1) | distinct_points(X1,X0) | ~spl9), inference(resolution, [status(thm)], [p664, p98])).
% 24.69/3.66 fof(sdef82, definition, (spl82 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk0,X1) | distinct_points(X1,X0))), introduced(definition, [new_symbols(naming, [spl82])], [avatar_definition])).
% 24.69/3.66 cnf(ssp67, plain, (~spl9 | spl23 | spl77 | spl82), inference(avatar_split_clause, [status(thm)], [p903, sdef23, sdef77, sdef82])).
% 24.69/3.66 cnf(p905, plain, (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk1,sk2)) | distinct_points(sk0,X0) | distinct_points(sk1,X1) | ~spl9), inference(resolution, [status(thm)], [p664, p99])).
% 24.69/3.66 fof(sdef83, definition, (spl83 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl83])], [avatar_definition])).
% 24.69/3.66 cnf(ssp68, plain, (~spl9 | spl78 | spl83), inference(avatar_split_clause, [status(thm)], [p905, sdef78, sdef83])).
% 24.69/3.66 cnf(p907, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(X0,sk1) | ~spl9), inference(resolution, [status(thm)], [p664, p100])).
% 24.69/3.66 fof(sdef84, definition, (spl84 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl84])], [avatar_definition])).
% 24.69/3.66 cnf(ssp69, plain, (~spl9 | spl21 | spl76 | spl84), inference(avatar_split_clause, [status(thm)], [p907, sdef21, sdef76, sdef84])).
% 24.69/3.66 cnf(p909, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk3,X1) | distinct_points(X0,X1) | ~spl9), inference(resolution, [status(thm)], [p664, p101])).
% 24.69/3.66 fof(sdef86, definition, (spl86 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk3,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl86])], [avatar_definition])).
% 24.69/3.66 cnf(ssp70, plain, (~spl9 | spl0 | spl85 | spl86), inference(avatar_split_clause, [status(thm)], [p909, sdef0, sdef85, sdef86])).
% 24.69/3.66 cnf(p912, plain, (apart_point_and_line(sk3,line_connecting(sk0,sk1)) | apart_point_and_line(sk3,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk2,X1) | distinct_points(X1,X0) | ~spl9), inference(resolution, [status(thm)], [p664, p102])).
% 24.69/3.66 fof(sdef87, definition, (spl87 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk2,X1) | distinct_points(X1,X0))), introduced(definition, [new_symbols(naming, [spl87])], [avatar_definition])).
% 24.69/3.66 cnf(ssp71, plain, (~spl9 | spl1 | spl79 | spl87), inference(avatar_split_clause, [status(thm)], [p912, sdef1, sdef79, sdef87])).
% 24.69/3.66 cnf(p914, plain, (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,line_connecting(sk1,sk2)) | distinct_points(sk2,X0) | distinct_points(sk3,X1) | ~spl9), inference(resolution, [status(thm)], [p664, p103])).
% 24.69/3.66 fof(sdef88, definition, (spl88 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk3,X0))), introduced(definition, [new_symbols(naming, [spl88])], [avatar_definition])).
% 24.69/3.66 cnf(ssp72, plain, (~spl9 | spl80 | spl88), inference(avatar_split_clause, [status(thm)], [p914, sdef80, sdef88])).
% 24.69/3.66 cnf(p916, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(X0,sk3) | ~spl9), inference(resolution, [status(thm)], [p664, p104])).
% 24.69/3.66 fof(sdef89, definition, (spl89 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(X0,sk3))), introduced(definition, [new_symbols(naming, [spl89])], [avatar_definition])).
% 24.69/3.66 cnf(ssp73, plain, (~spl9 | spl0 | spl85 | spl89), inference(avatar_split_clause, [status(thm)], [p916, sdef0, sdef85, sdef89])).
% 24.69/3.66 cnf(p918, plain, (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,line_connecting(sk1,sk2)) | distinct_points(sk0,X1) | distinct_points(X0,X1) | ~spl9), inference(resolution, [status(thm)], [p664, p105])).
% 24.69/3.66 fof(sdef90, definition, (spl90 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(sk0,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl90])], [avatar_definition])).
% 24.69/3.66 cnf(ssp74, plain, (~spl9 | spl23 | spl77 | spl90), inference(avatar_split_clause, [status(thm)], [p918, sdef23, sdef77, sdef90])).
% 24.69/3.66 cnf(p920, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,line_connecting(sk1,sk2)) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(X1,sk1) | distinct_points(X1,X0) | ~spl9), inference(resolution, [status(thm)], [p664, p106])).
% 24.69/3.66 fof(sdef91, definition, (spl91 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,line_connecting(sk1,sk2)) | distinct_points(X1,sk1) | distinct_points(X1,X0))), introduced(definition, [new_symbols(naming, [spl91])], [avatar_definition])).
% 24.69/3.66 cnf(ssp75, plain, (~spl9 | spl21 | spl76 | spl91), inference(avatar_split_clause, [status(thm)], [p920, sdef21, sdef76, sdef91])).
% 24.69/3.66 cnf(p930, plain, (distinct_points(sk1,sk3) | distinct_points(sk2,sk2) | ~spl77), inference(resolution, [status(thm)], [p895, p66])).
% 24.69/3.66 fof(sdef92, definition, (spl92 <=> (distinct_points(sk1,sk3))), introduced(definition, [new_symbols(naming, [spl92])], [avatar_definition])).
% 24.69/3.66 cnf(ssp76, plain, (~spl77 | spl2 | spl92), inference(avatar_split_clause, [status(thm)], [p930, sdef2, sdef92])).
% 24.69/3.66 cnf(p946, plain, (distinct_points(sk1,sk3) | distinct_points(sk2,sk2) | ~spl85), inference(resolution, [status(thm)], [p910, p90])).
% 24.69/3.66 cnf(ssp77, plain, (~spl85 | spl2 | spl92), inference(avatar_split_clause, [status(thm)], [p946, sdef2, sdef92])).
% 24.69/3.66 cnf(p35, plain, distinct_points(X0,sk1) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [p29, c0])).
% 24.69/3.66 cnf(p108, plain, ~distinct_lines(X0,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_points(X2,sk0), inference(resolution, [status(thm)], [c10, p35])).
% 24.69/3.66 cnf(p948, plain, (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,X1) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X1) | distinct_points(X0,sk0) | apart_point_and_line(sk3,X1) | ~spl1), inference(resolution, [status(thm)], [p108, p116])).
% 24.69/3.66 fof(sdef93, definition, (spl93 <=> (apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,X1) | apart_point_and_line(sk1,X1) | distinct_points(X0,sk0) | apart_point_and_line(sk3,X1))), introduced(definition, [new_symbols(naming, [spl93])], [avatar_definition])).
% 24.69/3.66 cnf(ssp78, plain, (~spl1 | spl23 | spl93), inference(avatar_split_clause, [status(thm)], [p948, sdef23, sdef93])).
% 24.69/3.66 cnf(p110, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(X3,sk3) | distinct_points(X3,X2), inference(resolution, [status(thm)], [c10, p34])).
% 24.69/3.66 cnf(p964, plain, (apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk3) | distinct_points(X2,X1) | apart_point_and_line(sk3,X0) | ~spl1), inference(resolution, [status(thm)], [p110, p116])).
% 24.69/3.66 fof(sdef94, definition, (spl94 <=> (apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk3) | distinct_points(X2,X1) | apart_point_and_line(sk3,X0))), introduced(definition, [new_symbols(naming, [spl94])], [avatar_definition])).
% 24.69/3.66 cnf(ssp79, plain, (~spl1 | spl0 | spl94), inference(avatar_split_clause, [status(thm)], [p964, sdef0, sdef94])).
% 24.69/3.66 cnf(p716, plain, (apart_point_and_line(sk1,line_connecting(sk3,sk2)) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 24.69/3.66 cnf(p720, plain, (distinct_lines(line_connecting(sk3,sk2),X0) | apart_point_and_line(sk1,X0) | ~spl29), inference(resolution, [status(thm)], [p716, c12])).
% 24.69/3.66 cnf(p94, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk2,X1) | apart_point_and_line(sk3,X0) | apart_point_and_line(sk3,X1), inference(resolution, [status(thm)], [c10, c15])).
% 24.69/3.66 cnf(p1106, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk3,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk3,line_connecting(sk3,sk2)) | apart_point_and_line(sk3,X0) | ~spl29), inference(resolution, [status(thm)], [p720, p94])).
% 24.69/3.66 fof(sdef95, definition, (spl95 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk3,X0))), introduced(definition, [new_symbols(naming, [spl95])], [avatar_definition])).
% 24.69/3.66 cnf(ssp80, plain, (~spl29 | spl38 | spl95 | spl96), inference(avatar_split_clause, [status(thm)], [p1106, sdef38, sdef95, sdef96])).
% 24.69/3.66 cnf(p1109, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk3,line_connecting(sk3,sk2)) | apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | ~spl29), inference(resolution, [status(thm)], [p720, p96])).
% 24.69/3.66 fof(sdef97, definition, (spl97 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1))), introduced(definition, [new_symbols(naming, [spl97])], [avatar_definition])).
% 24.69/3.66 cnf(ssp81, plain, (~spl29 | spl38 | spl97), inference(avatar_split_clause, [status(thm)], [p1109, sdef38, sdef97])).
% 24.69/3.66 cnf(p1111, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk0,line_connecting(sk3,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | ~spl29), inference(resolution, [status(thm)], [p720, p97])).
% 24.69/3.66 fof(sdef98, definition, (spl98 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl98])], [avatar_definition])).
% 24.69/3.66 cnf(ssp82, plain, (~spl29 | spl28 | spl98), inference(avatar_split_clause, [status(thm)], [p1111, sdef28, sdef98])).
% 24.69/3.66 cnf(p1113, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk0,line_connecting(sk3,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk1) | ~spl29), inference(resolution, [status(thm)], [p720, p100])).
% 24.69/3.66 fof(sdef99, definition, (spl99 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk1))), introduced(definition, [new_symbols(naming, [spl99])], [avatar_definition])).
% 24.69/3.66 cnf(ssp83, plain, (~spl29 | spl28 | spl99), inference(avatar_split_clause, [status(thm)], [p1113, sdef28, sdef99])).
% 24.69/3.66 cnf(p1115, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk3,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk3,X2) | distinct_points(X1,X2) | ~spl29), inference(resolution, [status(thm)], [p720, p101])).
% 24.69/3.66 fof(sdef100, definition, (spl100 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk3,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl100])], [avatar_definition])).
% 24.69/3.66 cnf(ssp84, plain, (~spl29 | spl96 | spl100), inference(avatar_split_clause, [status(thm)], [p1115, sdef96, sdef100])).
% 24.69/3.66 cnf(p1117, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk3,line_connecting(sk3,sk2)) | apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk2,X2) | distinct_points(X2,X1) | ~spl29), inference(resolution, [status(thm)], [p720, p102])).
% 24.69/3.66 fof(sdef101, definition, (spl101 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk2,X2) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl101])], [avatar_definition])).
% 24.69/3.66 cnf(ssp85, plain, (~spl29 | spl38 | spl101), inference(avatar_split_clause, [status(thm)], [p1117, sdef38, sdef101])).
% 24.69/3.66 cnf(p1120, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk3,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk3) | ~spl29), inference(resolution, [status(thm)], [p720, p104])).
% 24.69/3.66 fof(sdef102, definition, (spl102 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk3))), introduced(definition, [new_symbols(naming, [spl102])], [avatar_definition])).
% 24.69/3.66 cnf(ssp86, plain, (~spl29 | spl96 | spl102), inference(avatar_split_clause, [status(thm)], [p1120, sdef96, sdef102])).
% 24.69/3.66 cnf(p1122, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk0,line_connecting(sk3,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk1) | distinct_points(X2,X1) | ~spl29), inference(resolution, [status(thm)], [p720, p106])).
% 24.69/3.66 fof(sdef103, definition, (spl103 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk1) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl103])], [avatar_definition])).
% 24.69/3.66 cnf(ssp87, plain, (~spl29 | spl28 | spl103), inference(avatar_split_clause, [status(thm)], [p1122, sdef28, sdef103])).
% 24.69/3.66 cnf(p109, plain, ~distinct_lines(X0,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | apart_point_and_line(sk3,X0) | apart_point_and_line(sk3,X1) | distinct_points(sk2,X3) | distinct_points(X2,X3), inference(resolution, [status(thm)], [c10, p34])).
% 24.69/3.66 cnf(p1125, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk3,line_connecting(sk3,sk2)) | apart_point_and_line(sk3,X0) | distinct_points(sk2,X2) | distinct_points(X1,X2) | ~spl29), inference(resolution, [status(thm)], [p720, p109])).
% 24.69/3.66 fof(sdef104, definition, (spl104 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk3,X0) | distinct_points(sk2,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl104])], [avatar_definition])).
% 24.69/3.66 cnf(ssp88, plain, (~spl29 | spl38 | spl104), inference(avatar_split_clause, [status(thm)], [p1125, sdef38, sdef104])).
% 24.69/3.66 cnf(p1127, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk3,sk2)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk3) | distinct_points(X2,X1) | ~spl29), inference(resolution, [status(thm)], [p720, p110])).
% 24.69/3.66 fof(sdef105, definition, (spl105 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk3) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl105])], [avatar_definition])).
% 24.69/3.66 cnf(ssp89, plain, (~spl29 | spl96 | spl105), inference(avatar_split_clause, [status(thm)], [p1127, sdef96, sdef105])).
% 24.69/3.66 cnf(p112, plain, ~distinct_lines(X0,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | apart_point_and_line(sk3,X0) | apart_point_and_line(sk3,X1) | distinct_points(X2,sk2), inference(resolution, [status(thm)], [c10, p40])).
% 24.69/3.66 cnf(p1130, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk3,line_connecting(sk3,sk2)) | apart_point_and_line(sk3,X0) | distinct_points(X1,sk2) | ~spl29), inference(resolution, [status(thm)], [p720, p112])).
% 24.69/3.66 fof(sdef106, definition, (spl106 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk3,sk2)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk3,X0) | distinct_points(X1,sk2))), introduced(definition, [new_symbols(naming, [spl106])], [avatar_definition])).
% 24.69/3.66 cnf(ssp90, plain, (~spl29 | spl38 | spl106), inference(avatar_split_clause, [status(thm)], [p1130, sdef38, sdef106])).
% 24.69/3.66 cnf(p728, plain, (apart_point_and_line(sk1,line_connecting(sk2,sk0)) | ~spl33), inference(avatar_component_clause, [status(thm)], [sdef33])).
% 24.69/3.66 cnf(p764, plain, (distinct_points(sk1,X0) | apart_point_and_line(X0,line_connecting(sk2,sk0)) | ~spl33), inference(resolution, [status(thm)], [p728, c11])).
% 24.69/3.66 cnf(p1133, plain, (distinct_points(sk1,sk2) | distinct_points(sk0,sk3) | ~spl33), inference(resolution, [status(thm)], [p764, p57])).
% 24.69/3.66 cnf(ssp91, plain, (~spl33 | spl63 | spl64), inference(avatar_split_clause, [status(thm)], [p1133, sdef63, sdef64])).
% 24.69/3.66 cnf(p39, plain, distinct_points(X0,sk0) | distinct_points(X0,X1) | distinct_points(sk1,X1), inference(resolution, [status(thm)], [p35, c3])).
% 24.69/3.66 cnf(p284, plain, distinct_points(X0,sk0) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [p39, c0])).
% 24.69/3.66 cnf(p295, plain, distinct_points(sk1,X0) | ~apart_point_and_line(X0,line_connecting(X0,sk0)), inference(resolution, [status(thm)], [p284, c6])).
% 24.69/3.66 cnf(p1136, plain, (distinct_points(sk1,sk2) | distinct_points(sk1,sk2) | ~spl33), inference(resolution, [status(thm)], [p764, p295])).
% 24.69/3.66 cnf(ssp92, plain, (~spl33 | spl63), inference(avatar_split_clause, [status(thm)], [p1136, sdef63])).
% 24.69/3.66 cnf(p1137, plain, (distinct_points(sk1,sk2) | distinct_points(sk3,X0) | distinct_points(sk0,X0) | ~spl33), inference(resolution, [status(thm)], [p764, p54])).
% 24.69/3.66 fof(sdef107, definition, (spl107 <=> (distinct_points(sk3,X0) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl107])], [avatar_definition])).
% 24.69/3.66 cnf(ssp93, plain, (~spl33 | spl63 | spl107), inference(avatar_split_clause, [status(thm)], [p1137, sdef63, sdef107])).
% 24.69/3.66 cnf(p56, plain, ~apart_point_and_line(X0,line_connecting(X0,X1)) | distinct_points(sk2,X0) | distinct_points(sk3,X1), inference(resolution, [status(thm)], [c6, p24])).
% 24.69/3.66 cnf(p1139, plain, (distinct_points(sk1,sk2) | distinct_points(sk2,sk2) | distinct_points(sk3,sk0) | ~spl33), inference(resolution, [status(thm)], [p764, p56])).
% 24.69/3.66 cnf(ssp94, plain, (~spl33 | spl2 | spl35 | spl63), inference(avatar_split_clause, [status(thm)], [p1139, sdef2, sdef35, sdef63])).
% 24.69/3.66 cnf(p61, plain, ~apart_point_and_line(X0,line_connecting(X0,X1)) | distinct_points(X0,sk1) | distinct_points(sk0,X1), inference(resolution, [status(thm)], [c6, p29])).
% 24.69/3.66 cnf(p1140, plain, (distinct_points(sk1,sk2) | distinct_points(sk2,sk1) | distinct_points(sk0,sk0) | ~spl33), inference(resolution, [status(thm)], [p764, p61])).
% 24.69/3.66 cnf(ssp95, plain, (~spl33 | spl36 | spl37 | spl63), inference(avatar_split_clause, [status(thm)], [p1140, sdef36, sdef37, sdef63])).
% 24.69/3.66 cnf(p1141, plain, (distinct_points(sk1,sk2) | distinct_points(X0,sk3) | distinct_points(X0,sk0) | ~spl33), inference(resolution, [status(thm)], [p764, p65])).
% 24.69/3.66 fof(sdef108, definition, (spl108 <=> (distinct_points(X0,sk3) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl108])], [avatar_definition])).
% 24.69/3.66 cnf(ssp96, plain, (~spl33 | spl63 | spl108), inference(avatar_split_clause, [status(thm)], [p1141, sdef63, sdef108])).
% 24.69/3.66 cnf(p26, plain, distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(sk0,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [p23, c3])).
% 24.69/3.66 cnf(p140, plain, distinct_points(sk1,X0) | distinct_points(sk0,X1) | distinct_points(X2,X1) | ~apart_point_and_line(X2,line_connecting(X2,X0)), inference(resolution, [status(thm)], [p26, c6])).
% 24.69/3.66 cnf(p1148, plain, distinct_points(sk1,X0) | distinct_points(sk0,X1) | ~apart_point_and_line(sk0,line_connecting(sk0,X0)), inference(factoring, [status(thm)], [p140])).
% 24.69/3.66 fof(sdef109, definition, (spl109 <=> (distinct_points(sk1,X0) | ~apart_point_and_line(sk0,line_connecting(sk0,X0)))), introduced(definition, [new_symbols(naming, [spl109])], [avatar_definition])).
% 24.69/3.66 cnf(ssp97, plain, (spl109 | spl110), inference(avatar_split_clause, [status(thm)], [p1148, sdef109, sdef110])).
% 24.69/3.66 cnf(p141, plain, distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(X1,X2) | ~apart_point_and_line(sk0,line_connecting(sk0,X2)), inference(resolution, [status(thm)], [p26, c6])).
% 24.69/3.66 cnf(p1155, plain, distinct_points(sk1,X0) | distinct_points(sk1,X1) | ~apart_point_and_line(sk0,line_connecting(sk0,X1)), inference(factoring, [status(thm)], [p141])).
% 24.69/3.66 cnf(ssp98, plain, (spl109 | spl111), inference(avatar_split_clause, [status(thm)], [p1155, sdef109, sdef111])).
% 24.69/3.66 cnf(p142, plain, distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(sk0,X2) | ~apart_point_and_line(X1,line_connecting(X1,X2)), inference(resolution, [status(thm)], [p26, c6])).
% 24.69/3.66 cnf(p1168, plain, (distinct_points(sk1,X0) | distinct_points(sk2,X0) | distinct_points(sk0,sk0) | distinct_points(sk1,sk2) | ~spl33), inference(resolution, [status(thm)], [p142, p764])).
% 24.69/3.66 fof(sdef112, definition, (spl112 <=> (distinct_points(sk1,X0) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl112])], [avatar_definition])).
% 24.69/3.66 cnf(ssp99, plain, (~spl33 | spl37 | spl63 | spl112), inference(avatar_split_clause, [status(thm)], [p1168, sdef37, sdef63, sdef112])).
% 24.69/3.66 cnf(p144, plain, distinct_points(sk1,X0) | distinct_points(sk0,X1) | distinct_points(X2,X1) | ~apart_point_and_line(X0,line_connecting(X2,X0)), inference(resolution, [status(thm)], [p26, c7])).
% 24.69/3.66 cnf(p1185, plain, distinct_points(sk1,X0) | distinct_points(sk0,X1) | ~apart_point_and_line(X0,line_connecting(sk0,X0)), inference(factoring, [status(thm)], [p144])).
% 24.69/3.66 fof(sdef113, definition, (spl113 <=> (distinct_points(sk1,X0) | ~apart_point_and_line(X0,line_connecting(sk0,X0)))), introduced(definition, [new_symbols(naming, [spl113])], [avatar_definition])).
% 24.69/3.66 cnf(ssp100, plain, (spl110 | spl113), inference(avatar_split_clause, [status(thm)], [p1185, sdef110, sdef113])).
% 24.69/3.66 cnf(p765, plain, (distinct_lines(line_connecting(sk2,sk0),X0) | apart_point_and_line(sk1,X0) | ~spl33), inference(resolution, [status(thm)], [p728, c12])).
% 24.69/3.66 cnf(p1188, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,X0) | apart_point_and_line(sk3,line_connecting(sk2,sk0)) | apart_point_and_line(sk3,X0) | ~spl33), inference(resolution, [status(thm)], [p765, p94])).
% 24.69/3.66 cnf(ssp101, plain, (~spl33 | spl40 | spl95 | spl114), inference(avatar_split_clause, [status(thm)], [p1188, sdef40, sdef95, sdef114])).
% 24.69/3.66 cnf(p1190, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk3,line_connecting(sk2,sk0)) | apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1) | ~spl33), inference(resolution, [status(thm)], [p765, p96])).
% 24.69/3.66 fof(sdef115, definition, (spl115 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk2,X1))), introduced(definition, [new_symbols(naming, [spl115])], [avatar_definition])).
% 24.69/3.66 cnf(ssp102, plain, (~spl33 | spl40 | spl115), inference(avatar_split_clause, [status(thm)], [p1190, sdef40, sdef115])).
% 24.69/3.66 cnf(p1192, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | ~spl33), inference(resolution, [status(thm)], [p765, p97])).
% 24.69/3.66 fof(sdef116, definition, (spl116 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl116])], [avatar_definition])).
% 24.69/3.66 cnf(ssp103, plain, (~spl33 | spl32 | spl116), inference(avatar_split_clause, [status(thm)], [p1192, sdef32, sdef116])).
% 24.69/3.66 cnf(p1194, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk1) | ~spl33), inference(resolution, [status(thm)], [p765, p100])).
% 24.69/3.66 fof(sdef117, definition, (spl117 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk1))), introduced(definition, [new_symbols(naming, [spl117])], [avatar_definition])).
% 24.69/3.66 cnf(ssp104, plain, (~spl33 | spl32 | spl117), inference(avatar_split_clause, [status(thm)], [p1194, sdef32, sdef117])).
% 24.69/3.66 cnf(p1196, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk3,X2) | distinct_points(X1,X2) | ~spl33), inference(resolution, [status(thm)], [p765, p101])).
% 24.69/3.66 fof(sdef118, definition, (spl118 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk3,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl118])], [avatar_definition])).
% 24.69/3.66 cnf(ssp105, plain, (~spl33 | spl114 | spl118), inference(avatar_split_clause, [status(thm)], [p1196, sdef114, sdef118])).
% 24.69/3.66 cnf(p1198, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk3,line_connecting(sk2,sk0)) | apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk2,X2) | distinct_points(X2,X1) | ~spl33), inference(resolution, [status(thm)], [p765, p102])).
% 24.69/3.66 fof(sdef119, definition, (spl119 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk2,X2) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl119])], [avatar_definition])).
% 24.69/3.66 cnf(ssp106, plain, (~spl33 | spl40 | spl119), inference(avatar_split_clause, [status(thm)], [p1198, sdef40, sdef119])).
% 24.69/3.66 cnf(p1201, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk3) | ~spl33), inference(resolution, [status(thm)], [p765, p104])).
% 24.69/3.66 fof(sdef120, definition, (spl120 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk3))), introduced(definition, [new_symbols(naming, [spl120])], [avatar_definition])).
% 24.69/3.66 cnf(ssp107, plain, (~spl33 | spl114 | spl120), inference(avatar_split_clause, [status(thm)], [p1201, sdef114, sdef120])).
% 24.69/3.66 cnf(p1203, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk1) | distinct_points(X2,X1) | ~spl33), inference(resolution, [status(thm)], [p765, p106])).
% 24.69/3.66 fof(sdef121, definition, (spl121 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk1) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl121])], [avatar_definition])).
% 24.69/3.66 cnf(ssp108, plain, (~spl33 | spl32 | spl121), inference(avatar_split_clause, [status(thm)], [p1203, sdef32, sdef121])).
% 24.69/3.66 cnf(p1206, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk3,line_connecting(sk2,sk0)) | apart_point_and_line(sk3,X0) | distinct_points(sk2,X2) | distinct_points(X1,X2) | ~spl33), inference(resolution, [status(thm)], [p765, p109])).
% 24.69/3.66 fof(sdef122, definition, (spl122 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk3,X0) | distinct_points(sk2,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl122])], [avatar_definition])).
% 24.69/3.66 cnf(ssp109, plain, (~spl33 | spl40 | spl122), inference(avatar_split_clause, [status(thm)], [p1206, sdef40, sdef122])).
% 24.69/3.66 cnf(p1208, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk3) | distinct_points(X2,X1) | ~spl33), inference(resolution, [status(thm)], [p765, p110])).
% 24.69/3.66 fof(sdef123, definition, (spl123 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk3) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl123])], [avatar_definition])).
% 24.69/3.66 cnf(ssp110, plain, (~spl33 | spl114 | spl123), inference(avatar_split_clause, [status(thm)], [p1208, sdef114, sdef123])).
% 24.69/3.66 cnf(p1211, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk3,line_connecting(sk2,sk0)) | apart_point_and_line(sk3,X0) | distinct_points(X1,sk2) | ~spl33), inference(resolution, [status(thm)], [p765, p112])).
% 24.69/3.66 fof(sdef124, definition, (spl124 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk3,X0) | distinct_points(X1,sk2))), introduced(definition, [new_symbols(naming, [spl124])], [avatar_definition])).
% 24.69/3.66 cnf(ssp111, plain, (~spl33 | spl40 | spl124), inference(avatar_split_clause, [status(thm)], [p1211, sdef40, sdef124])).
% 24.69/3.66 cnf(p1218, plain, (distinct_points(sk2,sk2) | distinct_points(sk3,sk0) | ~spl114), inference(resolution, [status(thm)], [p1189, p56])).
% 24.69/3.66 cnf(ssp112, plain, (~spl114 | spl2 | spl35), inference(avatar_split_clause, [status(thm)], [p1218, sdef2, sdef35])).
% 24.69/3.66 cnf(p1219, plain, (distinct_points(sk2,sk1) | distinct_points(sk0,sk0) | ~spl114), inference(resolution, [status(thm)], [p1189, p61])).
% 24.69/3.66 cnf(ssp113, plain, (~spl114 | spl36 | spl37), inference(avatar_split_clause, [status(thm)], [p1219, sdef36, sdef37])).
% 24.69/3.66 cnf(p1221, plain, (distinct_points(sk1,X0) | distinct_points(sk2,X0) | distinct_points(sk0,sk0) | ~spl114), inference(resolution, [status(thm)], [p1189, p142])).
% 24.69/3.66 cnf(ssp114, plain, (~spl114 | spl37 | spl112), inference(avatar_split_clause, [status(thm)], [p1221, sdef37, sdef112])).
% 24.69/3.66 cnf(p145, plain, distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(X1,X2) | ~apart_point_and_line(X2,line_connecting(sk0,X2)), inference(resolution, [status(thm)], [p26, c7])).
% 24.69/3.66 cnf(p1225, plain, distinct_points(sk1,X0) | distinct_points(sk1,X1) | ~apart_point_and_line(X1,line_connecting(sk0,X1)), inference(factoring, [status(thm)], [p145])).
% 24.69/3.66 cnf(ssp115, plain, (spl111 | spl113), inference(avatar_split_clause, [status(thm)], [p1225, sdef111, sdef113])).
% 24.69/3.66 cnf(p147, plain, distinct_points(X0,X1) | distinct_points(sk0,X2) | distinct_points(X0,X2) | ~distinct_lines(X3,X4) | apart_point_and_line(sk1,X3) | apart_point_and_line(sk1,X4) | apart_point_and_line(X1,X3) | apart_point_and_line(X1,X4), inference(resolution, [status(thm)], [p26, c10])).
% 24.69/3.66 cnf(p1243, plain, (distinct_points(X0,X1) | distinct_points(sk0,X2) | distinct_points(X0,X2) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X3) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X3) | apart_point_and_line(sk3,X3) | ~spl1), inference(resolution, [status(thm)], [p147, p116])).
% 24.69/3.66 fof(sdef125, definition, (spl125 <=> (distinct_points(X0,X1) | distinct_points(sk0,X2) | distinct_points(X0,X2) | apart_point_and_line(sk1,X3) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X3) | apart_point_and_line(sk3,X3))), introduced(definition, [new_symbols(naming, [spl125])], [avatar_definition])).
% 24.69/3.66 cnf(ssp116, plain, (~spl1 | spl23 | spl125), inference(avatar_split_clause, [status(thm)], [p1243, sdef23, sdef125])).
% 24.69/3.66 cnf(p753, plain, (apart_point_and_line(sk3,line_connecting(sk2,sk0)) | ~spl40), inference(avatar_component_clause, [status(thm)], [sdef40])).
% 24.69/3.66 cnf(p769, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,line_connecting(sk2,sk0)) | ~spl40), inference(resolution, [status(thm)], [p753, c11])).
% 24.69/3.66 cnf(p81, plain, ~apart_point_and_line(X0,line_connecting(sk2,X0)) | distinct_points(X0,sk3), inference(resolution, [status(thm)], [c7, p30])).
% 24.69/3.66 cnf(p1250, plain, (distinct_points(sk3,sk0) | distinct_points(sk0,sk3) | ~spl40), inference(resolution, [status(thm)], [p769, p81])).
% 24.69/3.66 cnf(ssp117, plain, (~spl40 | spl35 | spl64), inference(avatar_split_clause, [status(thm)], [p1250, sdef35, sdef64])).
% 24.69/3.66 cnf(p297, plain, distinct_points(sk1,X0) | ~apart_point_and_line(sk0,line_connecting(X0,sk0)), inference(resolution, [status(thm)], [p284, c7])).
% 24.69/3.66 cnf(p1252, plain, (distinct_points(sk3,sk0) | distinct_points(sk1,sk2) | ~spl40), inference(resolution, [status(thm)], [p769, p297])).
% 24.69/3.66 cnf(ssp118, plain, (~spl40 | spl35 | spl63), inference(avatar_split_clause, [status(thm)], [p1252, sdef35, sdef63])).
% 24.69/3.66 cnf(p78, plain, ~apart_point_and_line(X0,line_connecting(sk2,X0)) | distinct_points(sk3,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [c7, p24])).
% 24.69/3.66 cnf(p1253, plain, (distinct_points(sk3,sk0) | distinct_points(sk3,X0) | distinct_points(sk0,X0) | ~spl40), inference(resolution, [status(thm)], [p769, p78])).
% 24.69/3.66 cnf(ssp119, plain, (~spl40 | spl35 | spl107), inference(avatar_split_clause, [status(thm)], [p1253, sdef35, sdef107])).
% 24.69/3.66 cnf(p1254, plain, (distinct_points(sk3,sk0) | distinct_points(sk2,sk2) | distinct_points(sk3,sk0) | ~spl40), inference(resolution, [status(thm)], [p769, p80])).
% 24.69/3.66 cnf(ssp120, plain, (~spl40 | spl2 | spl35), inference(avatar_split_clause, [status(thm)], [p1254, sdef2, sdef35])).
% 24.69/3.66 cnf(p1255, plain, (distinct_points(sk3,sk0) | distinct_points(sk2,sk1) | distinct_points(sk0,sk0) | ~spl40), inference(resolution, [status(thm)], [p769, p85])).
% 24.69/3.66 cnf(ssp121, plain, (~spl40 | spl35 | spl36 | spl37), inference(avatar_split_clause, [status(thm)], [p1255, sdef35, sdef36, sdef37])).
% 24.69/3.66 cnf(p89, plain, ~apart_point_and_line(X0,line_connecting(sk2,X0)) | distinct_points(X1,sk3) | distinct_points(X1,X0), inference(resolution, [status(thm)], [c7, p34])).
% 24.69/3.66 cnf(p1256, plain, (distinct_points(sk3,sk0) | distinct_points(X0,sk3) | distinct_points(X0,sk0) | ~spl40), inference(resolution, [status(thm)], [p769, p89])).
% 24.69/3.66 cnf(ssp122, plain, (~spl40 | spl35 | spl108), inference(avatar_split_clause, [status(thm)], [p1256, sdef35, sdef108])).
% 24.69/3.66 cnf(p146, plain, distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(sk0,X2) | ~apart_point_and_line(X2,line_connecting(X1,X2)), inference(resolution, [status(thm)], [p26, c7])).
% 24.69/3.66 cnf(p1257, plain, (distinct_points(sk3,sk0) | distinct_points(sk1,X0) | distinct_points(sk2,X0) | distinct_points(sk0,sk0) | ~spl40), inference(resolution, [status(thm)], [p769, p146])).
% 24.69/3.66 cnf(ssp123, plain, (~spl40 | spl35 | spl37 | spl112), inference(avatar_split_clause, [status(thm)], [p1257, sdef35, sdef37, sdef112])).
% 24.69/3.66 cnf(p770, plain, (distinct_lines(line_connecting(sk2,sk0),X0) | apart_point_and_line(sk3,X0) | ~spl40), inference(resolution, [status(thm)], [p753, c12])).
% 24.69/3.66 cnf(p1260, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | ~spl40), inference(resolution, [status(thm)], [p770, p93])).
% 24.69/3.66 cnf(ssp124, plain, (~spl40 | spl24 | spl32 | spl33), inference(avatar_split_clause, [status(thm)], [p1260, sdef24, sdef32, sdef33])).
% 24.69/3.66 cnf(p1261, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | ~spl40), inference(resolution, [status(thm)], [p770, p95])).
% 24.69/3.66 fof(sdef126, definition, (spl126 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1))), introduced(definition, [new_symbols(naming, [spl126])], [avatar_definition])).
% 24.69/3.66 cnf(ssp125, plain, (~spl40 | spl33 | spl126), inference(avatar_split_clause, [status(thm)], [p1261, sdef33, sdef126])).
% 24.69/3.66 cnf(p1263, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | ~spl40), inference(resolution, [status(thm)], [p770, p97])).
% 24.69/3.66 fof(sdef127, definition, (spl127 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl127])], [avatar_definition])).
% 24.69/3.66 cnf(ssp126, plain, (~spl40 | spl32 | spl127), inference(avatar_split_clause, [status(thm)], [p1263, sdef32, sdef127])).
% 24.69/3.66 cnf(p1265, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X2) | distinct_points(X2,X1) | ~spl40), inference(resolution, [status(thm)], [p770, p98])).
% 24.69/3.66 fof(sdef128, definition, (spl128 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X2) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl128])], [avatar_definition])).
% 24.69/3.66 cnf(ssp127, plain, (~spl40 | spl33 | spl128), inference(avatar_split_clause, [status(thm)], [p1265, sdef33, sdef128])).
% 24.69/3.66 cnf(p1268, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk1) | ~spl40), inference(resolution, [status(thm)], [p770, p100])).
% 24.69/3.66 fof(sdef129, definition, (spl129 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk1))), introduced(definition, [new_symbols(naming, [spl129])], [avatar_definition])).
% 24.69/3.66 cnf(ssp128, plain, (~spl40 | spl32 | spl129), inference(avatar_split_clause, [status(thm)], [p1268, sdef32, sdef129])).
% 24.69/3.66 cnf(p1270, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk3,X2) | distinct_points(X1,X2) | ~spl40), inference(resolution, [status(thm)], [p770, p101])).
% 24.69/3.66 fof(sdef130, definition, (spl130 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(sk3,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl130])], [avatar_definition])).
% 24.69/3.66 cnf(ssp129, plain, (~spl40 | spl114 | spl130), inference(avatar_split_clause, [status(thm)], [p1270, sdef114, sdef130])).
% 24.69/3.66 cnf(p1272, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk3) | ~spl40), inference(resolution, [status(thm)], [p770, p104])).
% 24.69/3.66 fof(sdef131, definition, (spl131 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk3))), introduced(definition, [new_symbols(naming, [spl131])], [avatar_definition])).
% 24.69/3.66 cnf(ssp130, plain, (~spl40 | spl114 | spl131), inference(avatar_split_clause, [status(thm)], [p1272, sdef114, sdef131])).
% 24.69/3.66 cnf(p1274, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | distinct_points(sk0,X2) | distinct_points(X1,X2) | ~spl40), inference(resolution, [status(thm)], [p770, p105])).
% 24.69/3.66 fof(sdef132, definition, (spl132 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk1,X0) | distinct_points(sk0,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl132])], [avatar_definition])).
% 24.69/3.66 cnf(ssp131, plain, (~spl40 | spl33 | spl132), inference(avatar_split_clause, [status(thm)], [p1274, sdef33, sdef132])).
% 24.69/3.66 cnf(p1276, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk1) | distinct_points(X2,X1) | ~spl40), inference(resolution, [status(thm)], [p770, p106])).
% 24.69/3.66 fof(sdef133, definition, (spl133 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk1) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl133])], [avatar_definition])).
% 24.69/3.66 cnf(ssp132, plain, (~spl40 | spl32 | spl133), inference(avatar_split_clause, [status(thm)], [p1276, sdef32, sdef133])).
% 24.69/3.66 cnf(p1279, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | distinct_points(X1,sk0) | ~spl40), inference(resolution, [status(thm)], [p770, p108])).
% 24.69/3.66 fof(sdef134, definition, (spl134 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk1,X0) | distinct_points(X1,sk0))), introduced(definition, [new_symbols(naming, [spl134])], [avatar_definition])).
% 24.69/3.66 cnf(ssp133, plain, (~spl40 | spl33 | spl134), inference(avatar_split_clause, [status(thm)], [p1279, sdef33, sdef134])).
% 24.69/3.66 cnf(p1281, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk0)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk3) | distinct_points(X2,X1) | ~spl40), inference(resolution, [status(thm)], [p770, p110])).
% 24.69/3.66 fof(sdef135, definition, (spl135 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk0)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk3) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl135])], [avatar_definition])).
% 24.69/3.66 cnf(ssp134, plain, (~spl40 | spl114 | spl135), inference(avatar_split_clause, [status(thm)], [p1281, sdef114, sdef135])).
% 24.69/3.66 cnf(p1284, plain, (apart_point_and_line(sk3,X0) | distinct_points(X1,X2) | distinct_points(sk0,X3) | distinct_points(X1,X3) | apart_point_and_line(sk1,line_connecting(sk2,sk0)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X2,line_connecting(sk2,sk0)) | apart_point_and_line(X2,X0) | ~spl40), inference(resolution, [status(thm)], [p770, p147])).
% 24.69/3.66 fof(sdef136, definition, (spl136 <=> (apart_point_and_line(sk3,X0) | distinct_points(X1,X2) | distinct_points(sk0,X3) | distinct_points(X1,X3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X2,line_connecting(sk2,sk0)) | apart_point_and_line(X2,X0))), introduced(definition, [new_symbols(naming, [spl136])], [avatar_definition])).
% 24.69/3.66 cnf(ssp135, plain, (~spl40 | spl33 | spl136), inference(avatar_split_clause, [status(thm)], [p1284, sdef33, sdef136])).
% 24.69/3.66 cnf(p775, plain, (apart_point_and_line(sk0,line_connecting(sk2,sk1)) | ~spl44), inference(avatar_component_clause, [status(thm)], [sdef44])).
% 24.69/3.66 cnf(p786, plain, (distinct_points(sk0,X0) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | ~spl44), inference(resolution, [status(thm)], [p775, c11])).
% 24.69/3.66 cnf(p53, plain, ~apart_point_and_line(X0,line_connecting(X0,sk1)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [c6, p25])).
% 24.69/3.66 cnf(p1287, plain, (distinct_points(sk0,sk2) | distinct_points(sk0,sk2) | ~spl44), inference(resolution, [status(thm)], [p786, p53])).
% 24.69/3.66 fof(sdef138, definition, (spl138 <=> (distinct_points(sk0,sk2))), introduced(definition, [new_symbols(naming, [spl138])], [avatar_definition])).
% 24.69/3.66 cnf(ssp136, plain, (~spl44 | spl137 | spl138), inference(avatar_split_clause, [status(thm)], [p1287, sdef137, sdef138])).
% 24.69/3.66 cnf(p1290, plain, (distinct_points(sk0,sk2) | distinct_points(sk1,sk3) | ~spl44), inference(resolution, [status(thm)], [p786, p57])).
% 24.69/3.66 cnf(ssp137, plain, (~spl44 | spl92 | spl137), inference(avatar_split_clause, [status(thm)], [p1290, sdef92, sdef137])).
% 24.69/3.66 cnf(p62, plain, ~apart_point_and_line(X0,line_connecting(X0,sk1)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c6, p35])).
% 24.69/3.66 cnf(p1291, plain, (distinct_points(sk0,sk2) | distinct_points(sk2,sk0) | ~spl44), inference(resolution, [status(thm)], [p786, p62])).
% 24.69/3.66 cnf(ssp138, plain, (~spl44 | spl137 | spl139), inference(avatar_split_clause, [status(thm)], [p1291, sdef137, sdef139])).
% 24.69/3.66 cnf(p1295, plain, (distinct_points(sk0,sk2) | distinct_points(sk3,X0) | distinct_points(sk1,X0) | ~spl44), inference(resolution, [status(thm)], [p786, p54])).
% 24.69/3.66 fof(sdef140, definition, (spl140 <=> (distinct_points(sk3,X0) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl140])], [avatar_definition])).
% 24.69/3.66 cnf(ssp139, plain, (~spl44 | spl137 | spl140), inference(avatar_split_clause, [status(thm)], [p1295, sdef137, sdef140])).
% 24.69/3.66 cnf(p1297, plain, (distinct_points(sk0,sk2) | distinct_points(sk2,sk2) | distinct_points(sk3,sk1) | ~spl44), inference(resolution, [status(thm)], [p786, p56])).
% 24.69/3.66 cnf(ssp140, plain, (~spl44 | spl2 | spl52 | spl137), inference(avatar_split_clause, [status(thm)], [p1297, sdef2, sdef52, sdef137])).
% 24.69/3.66 cnf(p59, plain, ~apart_point_and_line(X0,line_connecting(X0,sk1)) | distinct_points(sk0,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [c6, p29])).
% 24.69/3.66 cnf(p1298, plain, (distinct_points(sk0,sk2) | distinct_points(sk0,X0) | distinct_points(sk2,X0) | ~spl44), inference(resolution, [status(thm)], [p786, p59])).
% 24.69/3.66 fof(sdef141, definition, (spl141 <=> (distinct_points(sk0,X0) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl141])], [avatar_definition])).
% 24.69/3.66 cnf(ssp141, plain, (~spl44 | spl137 | spl141), inference(avatar_split_clause, [status(thm)], [p1298, sdef137, sdef141])).
% 24.69/3.66 cnf(p1300, plain, (distinct_points(sk0,sk2) | distinct_points(X0,sk3) | distinct_points(X0,sk1) | ~spl44), inference(resolution, [status(thm)], [p786, p65])).
% 24.69/3.66 fof(sdef142, definition, (spl142 <=> (distinct_points(X0,sk3) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl142])], [avatar_definition])).
% 24.69/3.66 cnf(ssp142, plain, (~spl44 | spl137 | spl142), inference(avatar_split_clause, [status(thm)], [p1300, sdef137, sdef142])).
% 24.69/3.66 cnf(p149, plain, distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(X1,X2) | ~distinct_lines(X3,X4) | apart_point_and_line(sk0,X3) | apart_point_and_line(sk0,X4) | apart_point_and_line(X2,X3) | apart_point_and_line(X2,X4), inference(resolution, [status(thm)], [p26, c10])).
% 24.69/3.66 cnf(p1312, plain, (distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(X1,X2) | apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X3) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X3) | apart_point_and_line(sk3,X3) | ~spl1), inference(resolution, [status(thm)], [p149, p116])).
% 24.69/3.66 fof(sdef143, definition, (spl143 <=> (distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(X1,X2) | apart_point_and_line(sk0,X3) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X3) | apart_point_and_line(sk3,X3))), introduced(definition, [new_symbols(naming, [spl143])], [avatar_definition])).
% 24.69/3.66 cnf(ssp143, plain, (~spl1 | spl21 | spl143), inference(avatar_split_clause, [status(thm)], [p1312, sdef21, sdef143])).
% 24.69/3.66 cnf(p1314, plain, (distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(X1,X2) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X3) | apart_point_and_line(X2,line_connecting(sk2,sk0)) | apart_point_and_line(X2,X3) | apart_point_and_line(sk1,X3) | ~spl33), inference(resolution, [status(thm)], [p149, p765])).
% 24.69/3.66 fof(sdef144, definition, (spl144 <=> (distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(X1,X2) | apart_point_and_line(sk0,X3) | apart_point_and_line(X2,line_connecting(sk2,sk0)) | apart_point_and_line(X2,X3) | apart_point_and_line(sk1,X3))), introduced(definition, [new_symbols(naming, [spl144])], [avatar_definition])).
% 24.69/3.66 cnf(ssp144, plain, (~spl33 | spl32 | spl144), inference(avatar_split_clause, [status(thm)], [p1314, sdef32, sdef144])).
% 24.69/3.66 cnf(p1316, plain, (distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(X1,X2) | apart_point_and_line(sk0,line_connecting(sk2,sk0)) | apart_point_and_line(sk0,X3) | apart_point_and_line(X2,line_connecting(sk2,sk0)) | apart_point_and_line(X2,X3) | apart_point_and_line(sk3,X3) | ~spl40), inference(resolution, [status(thm)], [p149, p770])).
% 24.69/3.66 fof(sdef145, definition, (spl145 <=> (distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(X1,X2) | apart_point_and_line(sk0,X3) | apart_point_and_line(X2,line_connecting(sk2,sk0)) | apart_point_and_line(X2,X3) | apart_point_and_line(sk3,X3))), introduced(definition, [new_symbols(naming, [spl145])], [avatar_definition])).
% 24.69/3.66 cnf(ssp145, plain, (~spl40 | spl32 | spl145), inference(avatar_split_clause, [status(thm)], [p1316, sdef32, sdef145])).
% 24.69/3.66 cnf(p780, plain, (apart_point_and_line(sk3,line_connecting(sk2,sk1)) | ~spl47), inference(avatar_component_clause, [status(thm)], [sdef47])).
% 24.69/3.66 cnf(p806, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,line_connecting(sk2,sk1)) | ~spl47), inference(resolution, [status(thm)], [p780, c11])).
% 24.69/3.66 cnf(p77, plain, ~apart_point_and_line(sk1,line_connecting(X0,sk1)) | distinct_points(sk0,X0), inference(resolution, [status(thm)], [c7, p25])).
% 24.69/3.67 cnf(p1412, plain, (distinct_points(sk3,sk1) | distinct_points(sk0,sk2) | ~spl47), inference(resolution, [status(thm)], [p806, p77])).
% 24.69/3.67 cnf(ssp146, plain, (~spl47 | spl52 | spl137), inference(avatar_split_clause, [status(thm)], [p1412, sdef52, sdef137])).
% 24.69/3.67 cnf(p1414, plain, (distinct_points(sk3,sk1) | distinct_points(sk1,sk3) | ~spl47), inference(resolution, [status(thm)], [p806, p81])).
% 24.69/3.67 cnf(ssp147, plain, (~spl47 | spl52 | spl92), inference(avatar_split_clause, [status(thm)], [p1414, sdef52, sdef92])).
% 24.69/3.67 cnf(p86, plain, ~apart_point_and_line(sk1,line_connecting(X0,sk1)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c7, p35])).
% 24.69/3.67 cnf(p1415, plain, (distinct_points(sk3,sk1) | distinct_points(sk2,sk0) | ~spl47), inference(resolution, [status(thm)], [p806, p86])).
% 24.69/3.67 cnf(ssp148, plain, (~spl47 | spl52 | spl139), inference(avatar_split_clause, [status(thm)], [p1415, sdef52, sdef139])).
% 24.69/3.67 cnf(p1417, plain, (distinct_points(sk3,sk1) | distinct_points(sk3,X0) | distinct_points(sk1,X0) | ~spl47), inference(resolution, [status(thm)], [p806, p78])).
% 24.69/3.67 cnf(ssp149, plain, (~spl47 | spl52 | spl140), inference(avatar_split_clause, [status(thm)], [p1417, sdef52, sdef140])).
% 24.69/3.67 cnf(p1418, plain, (distinct_points(sk3,sk1) | distinct_points(sk2,sk2) | distinct_points(sk3,sk1) | ~spl47), inference(resolution, [status(thm)], [p806, p80])).
% 24.69/3.67 cnf(ssp150, plain, (~spl47 | spl2 | spl52), inference(avatar_split_clause, [status(thm)], [p1418, sdef2, sdef52])).
% 24.69/3.67 cnf(p83, plain, ~apart_point_and_line(sk1,line_connecting(X0,sk1)) | distinct_points(sk0,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [c7, p29])).
% 24.69/3.67 cnf(p1419, plain, (distinct_points(sk3,sk1) | distinct_points(sk0,X0) | distinct_points(sk2,X0) | ~spl47), inference(resolution, [status(thm)], [p806, p83])).
% 24.69/3.67 cnf(ssp151, plain, (~spl47 | spl52 | spl141), inference(avatar_split_clause, [status(thm)], [p1419, sdef52, sdef141])).
% 24.69/3.67 cnf(p1420, plain, (distinct_points(sk3,sk1) | distinct_points(X0,sk3) | distinct_points(X0,sk1) | ~spl47), inference(resolution, [status(thm)], [p806, p89])).
% 24.69/3.67 cnf(ssp152, plain, (~spl47 | spl52 | spl142), inference(avatar_split_clause, [status(thm)], [p1420, sdef52, sdef142])).
% 24.69/3.67 cnf(p807, plain, (distinct_lines(line_connecting(sk2,sk1),X0) | apart_point_and_line(sk3,X0) | ~spl47), inference(resolution, [status(thm)], [p780, c12])).
% 24.69/3.67 cnf(p1434, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | ~spl47), inference(resolution, [status(thm)], [p807, p93])).
% 24.69/3.67 cnf(ssp153, plain, (~spl47 | spl24 | spl44 | spl45), inference(avatar_split_clause, [status(thm)], [p1434, sdef24, sdef44, sdef45])).
% 24.69/3.67 cnf(p1435, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | ~spl47), inference(resolution, [status(thm)], [p807, p95])).
% 24.69/3.67 fof(sdef146, definition, (spl146 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1))), introduced(definition, [new_symbols(naming, [spl146])], [avatar_definition])).
% 24.69/3.67 cnf(ssp154, plain, (~spl47 | spl45 | spl146), inference(avatar_split_clause, [status(thm)], [p1435, sdef45, sdef146])).
% 24.69/3.67 cnf(p1437, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2) | ~spl47), inference(resolution, [status(thm)], [p807, p97])).
% 24.69/3.67 fof(sdef147, definition, (spl147 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk1,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl147])], [avatar_definition])).
% 24.69/3.67 cnf(ssp155, plain, (~spl47 | spl44 | spl147), inference(avatar_split_clause, [status(thm)], [p1437, sdef44, sdef147])).
% 24.69/3.67 cnf(p1439, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X2) | distinct_points(X2,X1) | ~spl47), inference(resolution, [status(thm)], [p807, p98])).
% 24.69/3.67 fof(sdef148, definition, (spl148 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X2) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl148])], [avatar_definition])).
% 24.69/3.67 cnf(ssp156, plain, (~spl47 | spl45 | spl148), inference(avatar_split_clause, [status(thm)], [p1439, sdef45, sdef148])).
% 24.69/3.67 cnf(p1442, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk1) | ~spl47), inference(resolution, [status(thm)], [p807, p100])).
% 24.69/3.67 fof(sdef149, definition, (spl149 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk1))), introduced(definition, [new_symbols(naming, [spl149])], [avatar_definition])).
% 24.69/3.67 cnf(ssp157, plain, (~spl47 | spl44 | spl149), inference(avatar_split_clause, [status(thm)], [p1442, sdef44, sdef149])).
% 24.69/3.67 cnf(p1444, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk3,X2) | distinct_points(X1,X2) | ~spl47), inference(resolution, [status(thm)], [p807, p101])).
% 24.69/3.67 fof(sdef150, definition, (spl150 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk3,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl150])], [avatar_definition])).
% 24.69/3.67 cnf(ssp158, plain, (~spl47 | spl150 | spl151), inference(avatar_split_clause, [status(thm)], [p1444, sdef150, sdef151])).
% 24.69/3.67 cnf(p1447, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk3) | ~spl47), inference(resolution, [status(thm)], [p807, p104])).
% 24.69/3.67 fof(sdef152, definition, (spl152 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X1,sk3))), introduced(definition, [new_symbols(naming, [spl152])], [avatar_definition])).
% 24.69/3.67 cnf(ssp159, plain, (~spl47 | spl151 | spl152), inference(avatar_split_clause, [status(thm)], [p1447, sdef151, sdef152])).
% 24.69/3.67 cnf(p1449, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | distinct_points(sk0,X2) | distinct_points(X1,X2) | ~spl47), inference(resolution, [status(thm)], [p807, p105])).
% 24.69/3.67 fof(sdef153, definition, (spl153 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk1,X0) | distinct_points(sk0,X2) | distinct_points(X1,X2))), introduced(definition, [new_symbols(naming, [spl153])], [avatar_definition])).
% 24.69/3.67 cnf(ssp160, plain, (~spl47 | spl45 | spl153), inference(avatar_split_clause, [status(thm)], [p1449, sdef45, sdef153])).
% 24.69/3.67 cnf(p1451, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk1) | distinct_points(X2,X1) | ~spl47), inference(resolution, [status(thm)], [p807, p106])).
% 24.69/3.67 fof(sdef154, definition, (spl154 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk0,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk1) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl154])], [avatar_definition])).
% 24.69/3.67 cnf(ssp161, plain, (~spl47 | spl44 | spl154), inference(avatar_split_clause, [status(thm)], [p1451, sdef44, sdef154])).
% 24.69/3.67 cnf(p1454, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | distinct_points(X1,sk0) | ~spl47), inference(resolution, [status(thm)], [p807, p108])).
% 24.69/3.67 fof(sdef155, definition, (spl155 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | apart_point_and_line(sk1,X0) | distinct_points(X1,sk0))), introduced(definition, [new_symbols(naming, [spl155])], [avatar_definition])).
% 24.69/3.67 cnf(ssp162, plain, (~spl47 | spl45 | spl155), inference(avatar_split_clause, [status(thm)], [p1454, sdef45, sdef155])).
% 24.69/3.67 cnf(p1456, plain, (apart_point_and_line(sk3,X0) | apart_point_and_line(sk2,line_connecting(sk2,sk1)) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk3) | distinct_points(X2,X1) | ~spl47), inference(resolution, [status(thm)], [p807, p110])).
% 24.69/3.67 fof(sdef156, definition, (spl156 <=> (apart_point_and_line(sk3,X0) | apart_point_and_line(sk2,X0) | apart_point_and_line(X1,line_connecting(sk2,sk1)) | apart_point_and_line(X1,X0) | distinct_points(X2,sk3) | distinct_points(X2,X1))), introduced(definition, [new_symbols(naming, [spl156])], [avatar_definition])).
% 24.69/3.67 cnf(ssp163, plain, (~spl47 | spl151 | spl156), inference(avatar_split_clause, [status(thm)], [p1456, sdef151, sdef156])).
% 24.69/3.67 cnf(p1459, plain, (apart_point_and_line(sk3,X0) | distinct_points(X1,X2) | distinct_points(sk0,X3) | distinct_points(X1,X3) | apart_point_and_line(sk1,line_connecting(sk2,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X2,line_connecting(sk2,sk1)) | apart_point_and_line(X2,X0) | ~spl47), inference(resolution, [status(thm)], [p807, p147])).
% 24.69/3.67 fof(sdef157, definition, (spl157 <=> (apart_point_and_line(sk3,X0) | distinct_points(X1,X2) | distinct_points(sk0,X3) | distinct_points(X1,X3) | apart_point_and_line(sk1,X0) | apart_point_and_line(X2,line_connecting(sk2,sk1)) | apart_point_and_line(X2,X0))), introduced(definition, [new_symbols(naming, [spl157])], [avatar_definition])).
% 24.69/3.67 cnf(ssp164, plain, (~spl47 | spl45 | spl157), inference(avatar_split_clause, [status(thm)], [p1459, sdef45, sdef157])).
% 24.69/3.67 cnf(p1462, plain, (apart_point_and_line(sk3,X0) | distinct_points(sk1,X1) | distinct_points(X2,X1) | distinct_points(X2,X3) | apart_point_and_line(sk0,line_connecting(sk2,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(X3,line_connecting(sk2,sk1)) | apart_point_and_line(X3,X0) | ~spl47), inference(resolution, [status(thm)], [p807, p149])).
% 24.69/3.67 fof(sdef158, definition, (spl158 <=> (apart_point_and_line(sk3,X0) | distinct_points(sk1,X1) | distinct_points(X2,X1) | distinct_points(X2,X3) | apart_point_and_line(sk0,X0) | apart_point_and_line(X3,line_connecting(sk2,sk1)) | apart_point_and_line(X3,X0))), introduced(definition, [new_symbols(naming, [spl158])], [avatar_definition])).
% 24.69/3.67 cnf(ssp165, plain, (~spl47 | spl44 | spl158), inference(avatar_split_clause, [status(thm)], [p1462, sdef44, sdef158])).
% 24.69/3.67 cnf(p1471, plain, (distinct_points(sk2,sk2) | distinct_points(sk3,sk1) | ~spl151), inference(resolution, [status(thm)], [p1446, p56])).
% 24.69/3.67 cnf(ssp166, plain, (~spl151 | spl2 | spl52), inference(avatar_split_clause, [status(thm)], [p1471, sdef2, sdef52])).
% 24.69/3.67 cnf(p813, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | ~spl55), inference(avatar_component_clause, [status(thm)], [sdef55])).
% 24.69/3.67 cnf(p857, plain, (distinct_points(sk1,X0) | apart_point_and_line(X0,line_connecting(sk0,sk2)) | ~spl55), inference(resolution, [status(thm)], [p813, c11])).
% 24.69/3.67 cnf(p76, plain, ~apart_point_and_line(X0,line_connecting(sk0,X0)) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [c7, p25])).
% 24.69/3.67 cnf(p1475, plain, (distinct_points(sk1,sk2) | distinct_points(sk2,sk1) | ~spl55), inference(resolution, [status(thm)], [p857, p76])).
% 24.69/3.67 cnf(ssp167, plain, (~spl55 | spl36 | spl63), inference(avatar_split_clause, [status(thm)], [p1475, sdef36, sdef63])).
% 24.69/3.67 cnf(p1478, plain, (distinct_points(sk1,sk2) | distinct_points(sk3,sk0) | ~spl55), inference(resolution, [status(thm)], [p857, p329])).
% 24.69/3.67 cnf(ssp168, plain, (~spl55 | spl35 | spl63), inference(avatar_split_clause, [status(thm)], [p1478, sdef35, sdef63])).
% 24.69/3.67 cnf(p73, plain, ~apart_point_and_line(X0,line_connecting(sk0,X0)) | distinct_points(sk1,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [c7, p23])).
% 24.69/3.67 cnf(p1479, plain, (distinct_points(sk1,sk2) | distinct_points(sk1,X0) | distinct_points(sk2,X0) | ~spl55), inference(resolution, [status(thm)], [p857, p73])).
% 24.69/3.67 cnf(ssp169, plain, (~spl55 | spl63 | spl112), inference(avatar_split_clause, [status(thm)], [p1479, sdef63, sdef112])).
% 24.69/3.67 cnf(p1480, plain, (distinct_points(sk1,sk2) | distinct_points(sk0,sk0) | distinct_points(sk1,sk2) | ~spl55), inference(resolution, [status(thm)], [p857, p75])).
% 24.69/3.67 cnf(ssp170, plain, (~spl55 | spl37 | spl63), inference(avatar_split_clause, [status(thm)], [p1480, sdef37, sdef63])).
% 24.69/3.67 cnf(p84, plain, ~apart_point_and_line(X0,line_connecting(sk0,X0)) | distinct_points(X1,sk1) | distinct_points(X1,X0), inference(resolution, [status(thm)], [c7, p29])).
% 24.69/3.67 cnf(p1481, plain, (distinct_points(sk1,sk2) | distinct_points(X0,sk1) | distinct_points(X0,sk2) | ~spl55), inference(resolution, [status(thm)], [p857, p84])).
% 24.69/3.67 fof(sdef159, definition, (spl159 <=> (distinct_points(X0,sk1) | distinct_points(X0,sk2))), introduced(definition, [new_symbols(naming, [spl159])], [avatar_definition])).
% 24.69/3.67 cnf(ssp171, plain, (~spl55 | spl63 | spl159), inference(avatar_split_clause, [status(thm)], [p1481, sdef63, sdef159])).
% 24.69/3.67 cnf(p1483, plain, (distinct_points(sk1,sk2) | distinct_points(sk0,sk3) | distinct_points(sk2,sk2) | ~spl55), inference(resolution, [status(thm)], [p857, p90])).
% 24.69/3.67 cnf(ssp172, plain, (~spl55 | spl2 | spl63 | spl64), inference(avatar_split_clause, [status(thm)], [p1483, sdef2, sdef63, sdef64])).
% 24.69/3.67 cnf(p1484, plain, (distinct_points(sk1,sk2) | distinct_points(sk1,sk2) | distinct_points(sk0,X0) | distinct_points(sk0,X0) | ~spl55), inference(resolution, [status(thm)], [p857, p144])).
% 24.69/3.67 cnf(ssp173, plain, (~spl55 | spl63 | spl160), inference(avatar_split_clause, [status(thm)], [p1484, sdef63, sdef160])).
% 24.69/3.67 cnf(p1486, plain, (distinct_points(sk1,sk2) | distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(X1,sk2) | ~spl55), inference(resolution, [status(thm)], [p857, p145])).
% 24.69/3.67 fof(sdef161, definition, (spl161 <=> (distinct_points(sk1,X0) | distinct_points(X1,X0) | distinct_points(X1,sk2))), introduced(definition, [new_symbols(naming, [spl161])], [avatar_definition])).
% 24.69/3.67 cnf(ssp174, plain, (~spl55 | spl63 | spl161), inference(avatar_split_clause, [status(thm)], [p1486, sdef63, sdef161])).
% 24.69/3.67 cnf(p27, plain, distinct_points(sk0,X0) | distinct_points(X0,X1) | distinct_points(sk1,X2) | distinct_points(X1,X2), inference(resolution, [status(thm)], [p23, c3])).
% 24.69/3.67 cnf(p165, plain, distinct_points(X0,X1) | distinct_points(sk1,X2) | distinct_points(X1,X2) | ~apart_point_and_line(X0,line_connecting(sk0,X0)), inference(resolution, [status(thm)], [p27, c7])).
% 24.69/3.67 cnf(p1492, plain, (distinct_points(sk1,sk2) | distinct_points(sk2,X0) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl55), inference(resolution, [status(thm)], [p857, p165])).
% 24.69/3.67 fof(sdef162, definition, (spl162 <=> (distinct_points(sk2,X0) | distinct_points(sk1,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl162])], [avatar_definition])).
% 24.69/3.67 cnf(ssp175, plain, (~spl55 | spl63 | spl162), inference(avatar_split_clause, [status(thm)], [p1492, sdef63, sdef162])).
% 24.69/3.67 cnf(p168, plain, distinct_points(sk0,X0) | distinct_points(X0,X1) | distinct_points(sk1,X2) | ~apart_point_and_line(X2,line_connecting(X1,X2)), inference(resolution, [status(thm)], [p27, c7])).
% 24.69/3.67 cnf(p1502, plain, (distinct_points(sk0,X0) | distinct_points(X0,sk0) | distinct_points(sk1,sk2) | distinct_points(sk1,sk2) | ~spl55), inference(resolution, [status(thm)], [p168, p857])).
% 24.69/3.67 cnf(ssp176, plain, (~spl55 | spl63 | spl163), inference(avatar_split_clause, [status(thm)], [p1502, sdef63, sdef163])).
% 24.69/3.67 cnf(p169, plain, distinct_points(X0,X1) | distinct_points(sk1,X2) | distinct_points(X1,X2) | ~distinct_lines(X3,X4) | apart_point_and_line(sk0,X3) | apart_point_and_line(sk0,X4) | apart_point_and_line(X0,X3) | apart_point_and_line(X0,X4), inference(resolution, [status(thm)], [p27, c10])).
% 24.69/3.67 cnf(p1512, plain, (distinct_points(X0,X1) | distinct_points(sk1,X2) | distinct_points(X1,X2) | apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X3) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,X3) | apart_point_and_line(sk3,X3) | ~spl1), inference(resolution, [status(thm)], [p169, p116])).
% 24.69/3.67 fof(sdef164, definition, (spl164 <=> (distinct_points(X0,X1) | distinct_points(sk1,X2) | distinct_points(X1,X2) | apart_point_and_line(sk0,X3) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | apart_point_and_line(X0,X3) | apart_point_and_line(sk3,X3))), introduced(definition, [new_symbols(naming, [spl164])], [avatar_definition])).
% 24.69/3.67 cnf(ssp177, plain, (~spl1 | spl21 | spl164), inference(avatar_split_clause, [status(thm)], [p1512, sdef21, sdef164])).
% 24.69/3.67 cnf(p170, plain, distinct_points(sk0,X0) | distinct_points(X0,X1) | distinct_points(X1,X2) | ~distinct_lines(X3,X4) | apart_point_and_line(sk1,X3) | apart_point_and_line(sk1,X4) | apart_point_and_line(X2,X3) | apart_point_and_line(X2,X4), inference(resolution, [status(thm)], [p27, c10])).
% 24.69/3.67 cnf(p1514, plain, (distinct_points(sk0,X0) | distinct_points(X0,X1) | distinct_points(X1,X2) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X3) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X3) | apart_point_and_line(sk3,X3) | ~spl1), inference(resolution, [status(thm)], [p170, p116])).
% 24.69/3.67 fof(sdef165, definition, (spl165 <=> (distinct_points(sk0,X0) | distinct_points(X0,X1) | distinct_points(X1,X2) | apart_point_and_line(sk1,X3) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X3) | apart_point_and_line(sk3,X3))), introduced(definition, [new_symbols(naming, [spl165])], [avatar_definition])).
% 24.69/3.67 cnf(ssp178, plain, (~spl1 | spl23 | spl165), inference(avatar_split_clause, [status(thm)], [p1514, sdef23, sdef165])).
% 24.69/3.67 cnf(p114, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,line_connecting(sk0,sk1)) | ~spl1), inference(resolution, [status(thm)], [c11, p20])).
% 24.69/3.67 cnf(p177, plain, (distinct_points(sk3,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | apart_point_and_line(X0,X1) | ~spl1), inference(resolution, [status(thm)], [p114, c12])).
% 24.69/3.67 cnf(p1557, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk2)) | ~spl1), inference(resolution, [status(thm)], [p177, p68])).
% 24.69/3.67 cnf(ssp179, plain, (~spl1 | spl4 | spl166), inference(avatar_split_clause, [status(thm)], [p1557, sdef4, sdef166])).
% 24.69/3.67 cnf(p70, plain, ~apart_point_and_line(sk3,line_connecting(sk2,sk3)), inference(resolution, [status(thm)], [c7, c15])).
% 24.69/3.67 cnf(p1559, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk2,sk3)) | ~spl1), inference(resolution, [status(thm)], [p177, p70])).
% 24.69/3.67 cnf(ssp180, plain, (~spl1 | spl3 | spl166), inference(avatar_split_clause, [status(thm)], [p1559, sdef3, sdef166])).
% 24.69/3.67 cnf(p48, plain, ~apart_point_and_line(sk3,line_connecting(sk3,X0)) | distinct_points(sk2,X0), inference(resolution, [status(thm)], [c6, p22])).
% 24.69/3.67 cnf(p1560, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk2,X0) | ~spl1), inference(resolution, [status(thm)], [p177, p48])).
% 24.69/3.67 fof(sdef167, definition, (spl167 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl167])], [avatar_definition])).
% 24.69/3.67 cnf(ssp181, plain, (~spl1 | spl166 | spl167), inference(avatar_split_clause, [status(thm)], [p1560, sdef166, sdef167])).
% 24.69/3.67 cnf(p82, plain, ~apart_point_and_line(sk3,line_connecting(X0,sk3)) | distinct_points(sk2,X0), inference(resolution, [status(thm)], [c7, p30])).
% 24.69/3.67 cnf(p1563, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(sk2,X0) | ~spl1), inference(resolution, [status(thm)], [p177, p82])).
% 24.69/3.67 fof(sdef168, definition, (spl168 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(sk2,X0))), introduced(definition, [new_symbols(naming, [spl168])], [avatar_definition])).
% 24.69/3.67 cnf(ssp182, plain, (~spl1 | spl166 | spl168), inference(avatar_split_clause, [status(thm)], [p1563, sdef166, sdef168])).
% 24.69/3.67 cnf(p91, plain, ~apart_point_and_line(sk3,line_connecting(X0,sk3)) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [c7, p40])).
% 24.69/3.67 cnf(p1565, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(X0,sk2) | ~spl1), inference(resolution, [status(thm)], [p177, p91])).
% 24.69/3.67 fof(sdef169, definition, (spl169 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(X0,sk2))), introduced(definition, [new_symbols(naming, [spl169])], [avatar_definition])).
% 24.69/3.67 cnf(ssp183, plain, (~spl1 | spl166 | spl169), inference(avatar_split_clause, [status(thm)], [p1565, sdef166, sdef169])).
% 24.69/3.67 cnf(p174, plain, (distinct_points(sk3,sk0) | ~spl1), inference(resolution, [status(thm)], [p114, p45])).
% 24.69/3.67 cnf(p191, plain, (~apart_point_and_line(sk3,line_connecting(sk3,sk0)) | ~spl1), inference(resolution, [status(thm)], [p174, c6])).
% 24.69/3.67 cnf(p1568, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk0)) | ~spl1), inference(resolution, [status(thm)], [p177, p191])).
% 24.69/3.67 fof(sdef170, definition, (spl170 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk0)))), introduced(definition, [new_symbols(naming, [spl170])], [avatar_definition])).
% 24.69/3.67 cnf(ssp184, plain, (~spl1 | spl166 | spl170), inference(avatar_split_clause, [status(thm)], [p1568, sdef166, sdef170])).
% 24.69/3.67 cnf(p175, plain, (distinct_points(sk3,sk1) | ~spl1), inference(resolution, [status(thm)], [p114, p69])).
% 24.69/3.67 cnf(p195, plain, (~apart_point_and_line(sk3,line_connecting(sk3,sk1)) | ~spl1), inference(resolution, [status(thm)], [p175, c6])).
% 24.69/3.67 cnf(p1570, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk1)) | ~spl1), inference(resolution, [status(thm)], [p177, p195])).
% 24.69/3.67 fof(sdef171, definition, (spl171 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,sk1)))), introduced(definition, [new_symbols(naming, [spl171])], [avatar_definition])).
% 24.69/3.67 cnf(ssp185, plain, (~spl1 | spl166 | spl171), inference(avatar_split_clause, [status(thm)], [p1570, sdef166, sdef171])).
% 24.69/3.67 cnf(p190, plain, (distinct_points(sk3,X0) | distinct_points(sk0,X0) | ~spl1), inference(resolution, [status(thm)], [p174, c3])).
% 24.69/3.67 cnf(p215, plain, (distinct_points(sk0,sk3) | ~spl1), inference(resolution, [status(thm)], [p190, c0])).
% 24.69/3.67 cnf(p221, plain, (~apart_point_and_line(sk3,line_connecting(sk0,sk3)) | ~spl1), inference(resolution, [status(thm)], [p215, c7])).
% 24.69/3.67 cnf(p1572, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk3)) | ~spl1), inference(resolution, [status(thm)], [p177, p221])).
% 24.69/3.67 fof(sdef172, definition, (spl172 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk3)))), introduced(definition, [new_symbols(naming, [spl172])], [avatar_definition])).
% 24.69/3.67 cnf(ssp186, plain, (~spl1 | spl166 | spl172), inference(avatar_split_clause, [status(thm)], [p1572, sdef166, sdef172])).
% 24.69/3.67 cnf(p194, plain, (distinct_points(sk3,X0) | distinct_points(sk1,X0) | ~spl1), inference(resolution, [status(thm)], [p175, c3])).
% 24.69/3.67 cnf(p236, plain, (distinct_points(sk1,sk3) | ~spl1), inference(resolution, [status(thm)], [p194, c0])).
% 24.69/3.67 cnf(p242, plain, (~apart_point_and_line(sk3,line_connecting(sk1,sk3)) | ~spl1), inference(resolution, [status(thm)], [p236, c7])).
% 24.69/3.67 cnf(p1574, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk3)) | ~spl1), inference(resolution, [status(thm)], [p177, p242])).
% 24.69/3.67 fof(sdef173, definition, (spl173 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk1,sk3)))), introduced(definition, [new_symbols(naming, [spl173])], [avatar_definition])).
% 24.69/3.67 cnf(ssp187, plain, (~spl1 | spl166 | spl173), inference(avatar_split_clause, [status(thm)], [p1574, sdef166, sdef173])).
% 24.69/3.67 cnf(p217, plain, (distinct_points(sk0,X0) | ~apart_point_and_line(sk3,line_connecting(sk3,X0)) | ~spl1), inference(resolution, [status(thm)], [p190, c6])).
% 24.69/3.67 cnf(p1576, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk0,X0) | ~spl1), inference(resolution, [status(thm)], [p177, p217])).
% 24.69/3.67 fof(sdef174, definition, (spl174 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl174])], [avatar_definition])).
% 24.69/3.67 cnf(ssp188, plain, (~spl1 | spl166 | spl174), inference(avatar_split_clause, [status(thm)], [p1576, sdef166, sdef174])).
% 24.69/3.67 cnf(p238, plain, (distinct_points(sk1,X0) | ~apart_point_and_line(sk3,line_connecting(sk3,X0)) | ~spl1), inference(resolution, [status(thm)], [p194, c6])).
% 24.69/3.67 cnf(p1578, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk1,X0) | ~spl1), inference(resolution, [status(thm)], [p177, p238])).
% 24.69/3.67 fof(sdef175, definition, (spl175 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl175])], [avatar_definition])).
% 24.69/3.67 cnf(ssp189, plain, (~spl1 | spl166 | spl175), inference(avatar_split_clause, [status(thm)], [p1578, sdef166, sdef175])).
% 24.69/3.67 cnf(p328, plain, distinct_points(X0,sk2) | ~apart_point_and_line(sk3,line_connecting(sk3,X0)), inference(resolution, [status(thm)], [p316, c6])).
% 24.69/3.67 cnf(p1581, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(X0,sk2) | ~spl1), inference(resolution, [status(thm)], [p177, p328])).
% 24.69/3.67 fof(sdef176, definition, (spl176 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(X0,sk2))), introduced(definition, [new_symbols(naming, [spl176])], [avatar_definition])).
% 24.69/3.67 cnf(ssp190, plain, (~spl1 | spl166 | spl176), inference(avatar_split_clause, [status(thm)], [p1581, sdef166, sdef176])).
% 24.69/3.67 cnf(p55, plain, ~apart_point_and_line(sk3,line_connecting(sk3,X0)) | distinct_points(sk2,X1) | distinct_points(X1,X0), inference(resolution, [status(thm)], [c6, p24])).
% 24.69/3.67 cnf(p1583, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk2,X1) | distinct_points(X1,X0) | ~spl1), inference(resolution, [status(thm)], [p177, p55])).
% 24.69/3.67 fof(sdef177, definition, (spl177 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(sk2,X1) | distinct_points(X1,X0))), introduced(definition, [new_symbols(naming, [spl177])], [avatar_definition])).
% 24.69/3.67 cnf(ssp191, plain, (~spl1 | spl166 | spl177), inference(avatar_split_clause, [status(thm)], [p1583, sdef166, sdef177])).
% 24.69/3.67 cnf(p216, plain, (distinct_points(sk0,X0) | distinct_points(sk3,X1) | distinct_points(X0,X1) | ~spl1), inference(resolution, [status(thm)], [p190, c3])).
% 24.69/3.67 cnf(p405, plain, (distinct_points(sk0,X0) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p216, c0])).
% 24.69/3.67 cnf(p422, plain, (distinct_points(sk0,X0) | ~apart_point_and_line(sk3,line_connecting(X0,sk3)) | ~spl1), inference(resolution, [status(thm)], [p405, c7])).
% 24.69/3.67 cnf(p1586, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(sk0,X0) | ~spl1), inference(resolution, [status(thm)], [p177, p422])).
% 24.69/3.67 fof(sdef178, definition, (spl178 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(sk0,X0))), introduced(definition, [new_symbols(naming, [spl178])], [avatar_definition])).
% 24.69/3.67 cnf(ssp192, plain, (~spl1 | spl166 | spl178), inference(avatar_split_clause, [status(thm)], [p1586, sdef166, sdef178])).
% 24.69/3.67 cnf(p237, plain, (distinct_points(sk1,X0) | distinct_points(sk3,X1) | distinct_points(X0,X1) | ~spl1), inference(resolution, [status(thm)], [p194, c3])).
% 24.69/3.67 cnf(p432, plain, (distinct_points(sk1,X0) | distinct_points(X0,sk3) | ~spl1), inference(resolution, [status(thm)], [p237, c0])).
% 24.69/3.67 cnf(p449, plain, (distinct_points(sk1,X0) | ~apart_point_and_line(sk3,line_connecting(X0,sk3)) | ~spl1), inference(resolution, [status(thm)], [p432, c7])).
% 24.69/3.67 cnf(p1589, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(sk1,X0) | ~spl1), inference(resolution, [status(thm)], [p177, p449])).
% 24.69/3.67 fof(sdef179, definition, (spl179 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(sk1,X0))), introduced(definition, [new_symbols(naming, [spl179])], [avatar_definition])).
% 24.69/3.67 cnf(ssp193, plain, (~spl1 | spl166 | spl179), inference(avatar_split_clause, [status(thm)], [p1589, sdef166, sdef179])).
% 24.69/3.67 cnf(p418, plain, (distinct_points(X0,sk3) | distinct_points(sk0,X1) | distinct_points(X0,X1) | ~spl1), inference(resolution, [status(thm)], [p405, c3])).
% 24.69/3.67 cnf(p503, plain, (distinct_points(X0,sk3) | distinct_points(X0,sk0) | ~spl1), inference(resolution, [status(thm)], [p418, c0])).
% 24.69/3.67 cnf(p517, plain, (distinct_points(X0,sk0) | ~apart_point_and_line(sk3,line_connecting(X0,sk3)) | ~spl1), inference(resolution, [status(thm)], [p503, c7])).
% 24.69/3.67 cnf(p1591, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(X0,sk0) | ~spl1), inference(resolution, [status(thm)], [p177, p517])).
% 24.69/3.67 fof(sdef180, definition, (spl180 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl180])], [avatar_definition])).
% 24.69/3.67 cnf(ssp194, plain, (~spl1 | spl166 | spl180), inference(avatar_split_clause, [status(thm)], [p1591, sdef166, sdef180])).
% 24.69/3.67 cnf(p445, plain, (distinct_points(X0,sk3) | distinct_points(sk1,X1) | distinct_points(X0,X1) | ~spl1), inference(resolution, [status(thm)], [p432, c3])).
% 24.69/3.67 cnf(p519, plain, (distinct_points(X0,sk3) | distinct_points(X0,sk1) | ~spl1), inference(resolution, [status(thm)], [p445, c0])).
% 24.69/3.67 cnf(p533, plain, (distinct_points(X0,sk1) | ~apart_point_and_line(sk3,line_connecting(X0,sk3)) | ~spl1), inference(resolution, [status(thm)], [p519, c7])).
% 24.69/3.67 cnf(p1594, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(X0,sk1) | ~spl1), inference(resolution, [status(thm)], [p177, p533])).
% 24.69/3.67 fof(sdef181, definition, (spl181 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl181])], [avatar_definition])).
% 24.69/3.67 cnf(ssp195, plain, (~spl1 | spl166 | spl181), inference(avatar_split_clause, [status(thm)], [p1594, sdef166, sdef181])).
% 24.69/3.67 cnf(p515, plain, (distinct_points(X0,sk0) | distinct_points(X0,X1) | distinct_points(sk3,X1) | ~spl1), inference(resolution, [status(thm)], [p503, c3])).
% 24.69/3.67 cnf(p569, plain, (distinct_points(X0,sk0) | distinct_points(sk3,X0) | ~spl1), inference(resolution, [status(thm)], [p515, c0])).
% 24.69/3.67 cnf(p582, plain, (distinct_points(X0,sk0) | ~apart_point_and_line(sk3,line_connecting(sk3,X0)) | ~spl1), inference(resolution, [status(thm)], [p569, c6])).
% 24.69/3.67 cnf(p1598, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(X0,sk0) | ~spl1), inference(resolution, [status(thm)], [p177, p582])).
% 24.69/3.67 fof(sdef182, definition, (spl182 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(X0,sk0))), introduced(definition, [new_symbols(naming, [spl182])], [avatar_definition])).
% 24.69/3.67 cnf(ssp196, plain, (~spl1 | spl166 | spl182), inference(avatar_split_clause, [status(thm)], [p1598, sdef166, sdef182])).
% 24.69/3.67 cnf(p531, plain, (distinct_points(X0,sk1) | distinct_points(X0,X1) | distinct_points(sk3,X1) | ~spl1), inference(resolution, [status(thm)], [p519, c3])).
% 24.69/3.67 cnf(p586, plain, (distinct_points(X0,sk1) | distinct_points(sk3,X0) | ~spl1), inference(resolution, [status(thm)], [p531, c0])).
% 24.69/3.67 cnf(p599, plain, (distinct_points(X0,sk1) | ~apart_point_and_line(sk3,line_connecting(sk3,X0)) | ~spl1), inference(resolution, [status(thm)], [p586, c6])).
% 24.69/3.67 cnf(p1601, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(X0,sk1) | ~spl1), inference(resolution, [status(thm)], [p177, p599])).
% 24.69/3.67 fof(sdef183, definition, (spl183 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk3,X0)) | distinct_points(X0,sk1))), introduced(definition, [new_symbols(naming, [spl183])], [avatar_definition])).
% 24.69/3.67 cnf(ssp197, plain, (~spl1 | spl166 | spl183), inference(avatar_split_clause, [status(thm)], [p1601, sdef166, sdef183])).
% 24.69/3.67 cnf(p88, plain, ~apart_point_and_line(sk3,line_connecting(X0,sk3)) | distinct_points(sk2,X1) | distinct_points(X0,X1), inference(resolution, [status(thm)], [c7, p34])).
% 24.69/3.67 cnf(p1604, plain, (distinct_points(sk3,sk3) | distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(sk2,X1) | distinct_points(X0,X1) | ~spl1), inference(resolution, [status(thm)], [p177, p88])).
% 24.69/3.67 fof(sdef184, definition, (spl184 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(X0,sk3)) | distinct_points(sk2,X1) | distinct_points(X0,X1))), introduced(definition, [new_symbols(naming, [spl184])], [avatar_definition])).
% 24.69/3.67 cnf(ssp198, plain, (~spl1 | spl166 | spl184), inference(avatar_split_clause, [status(thm)], [p1604, sdef166, sdef184])).
% 24.69/3.67 cnf(p1607, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X1) | ~spl1), inference(resolution, [status(thm)], [p177, p93])).
% 24.69/3.67 fof(sdef185, definition, (spl185 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X1))), introduced(definition, [new_symbols(naming, [spl185])], [avatar_definition])).
% 24.69/3.67 cnf(ssp199, plain, (~spl1 | spl21 | spl23 | spl185), inference(avatar_split_clause, [status(thm)], [p1607, sdef21, sdef23, sdef185])).
% 24.69/3.67 cnf(p1609, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(sk0,X2) | ~spl1), inference(resolution, [status(thm)], [p177, p95])).
% 24.69/3.67 fof(sdef186, definition, (spl186 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk1,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(sk0,X2))), introduced(definition, [new_symbols(naming, [spl186])], [avatar_definition])).
% 24.69/3.67 cnf(ssp200, plain, (~spl1 | spl23 | spl186), inference(avatar_split_clause, [status(thm)], [p1609, sdef23, sdef186])).
% 24.69/3.67 cnf(p1611, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(sk1,X3) | distinct_points(X2,X3) | ~spl1), inference(resolution, [status(thm)], [p177, p97])).
% 24.69/3.67 fof(sdef187, definition, (spl187 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk0,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(sk1,X3) | distinct_points(X2,X3))), introduced(definition, [new_symbols(naming, [spl187])], [avatar_definition])).
% 24.69/3.67 cnf(ssp201, plain, (~spl1 | spl21 | spl187), inference(avatar_split_clause, [status(thm)], [p1611, sdef21, sdef187])).
% 24.69/3.67 cnf(p1613, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(sk0,X3) | distinct_points(X3,X2) | ~spl1), inference(resolution, [status(thm)], [p177, p98])).
% 24.69/3.67 fof(sdef188, definition, (spl188 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk1,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(sk0,X3) | distinct_points(X3,X2))), introduced(definition, [new_symbols(naming, [spl188])], [avatar_definition])).
% 24.69/3.67 cnf(ssp202, plain, (~spl1 | spl23 | spl188), inference(avatar_split_clause, [status(thm)], [p1613, sdef23, sdef188])).
% 24.69/3.67 cnf(p1616, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(X2,sk1) | ~spl1), inference(resolution, [status(thm)], [p177, p100])).
% 24.69/3.67 fof(sdef189, definition, (spl189 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk0,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(X2,sk1))), introduced(definition, [new_symbols(naming, [spl189])], [avatar_definition])).
% 24.69/3.67 cnf(ssp203, plain, (~spl1 | spl21 | spl189), inference(avatar_split_clause, [status(thm)], [p1616, sdef21, sdef189])).
% 24.69/3.67 cnf(p1618, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(sk3,X3) | distinct_points(X2,X3) | ~spl1), inference(resolution, [status(thm)], [p177, p101])).
% 24.69/3.67 fof(sdef190, definition, (spl190 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk2,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(sk3,X3) | distinct_points(X2,X3))), introduced(definition, [new_symbols(naming, [spl190])], [avatar_definition])).
% 24.69/3.67 cnf(ssp204, plain, (~spl1 | spl0 | spl190), inference(avatar_split_clause, [status(thm)], [p1618, sdef0, sdef190])).
% 24.69/3.67 cnf(p1620, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(X2,sk3) | ~spl1), inference(resolution, [status(thm)], [p177, p104])).
% 24.69/3.67 fof(sdef191, definition, (spl191 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk2,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(X2,sk3))), introduced(definition, [new_symbols(naming, [spl191])], [avatar_definition])).
% 24.69/3.67 cnf(ssp205, plain, (~spl1 | spl0 | spl191), inference(avatar_split_clause, [status(thm)], [p1620, sdef0, sdef191])).
% 24.69/3.67 cnf(p1622, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X1) | distinct_points(sk0,X3) | distinct_points(X2,X3) | ~spl1), inference(resolution, [status(thm)], [p177, p105])).
% 24.69/3.67 fof(sdef192, definition, (spl192 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | apart_point_and_line(sk1,X1) | distinct_points(sk0,X3) | distinct_points(X2,X3))), introduced(definition, [new_symbols(naming, [spl192])], [avatar_definition])).
% 24.69/3.67 cnf(ssp206, plain, (~spl1 | spl23 | spl192), inference(avatar_split_clause, [status(thm)], [p1622, sdef23, sdef192])).
% 24.69/3.67 cnf(p1624, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(X3,sk1) | distinct_points(X3,X2) | ~spl1), inference(resolution, [status(thm)], [p177, p106])).
% 24.69/3.67 fof(sdef193, definition, (spl193 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk0,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(X3,sk1) | distinct_points(X3,X2))), introduced(definition, [new_symbols(naming, [spl193])], [avatar_definition])).
% 24.69/3.67 cnf(ssp207, plain, (~spl1 | spl21 | spl193), inference(avatar_split_clause, [status(thm)], [p1624, sdef21, sdef193])).
% 24.69/3.67 cnf(p1627, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X1) | distinct_points(X2,sk0) | ~spl1), inference(resolution, [status(thm)], [p177, p108])).
% 24.69/3.67 fof(sdef194, definition, (spl194 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | apart_point_and_line(sk1,X1) | distinct_points(X2,sk0))), introduced(definition, [new_symbols(naming, [spl194])], [avatar_definition])).
% 24.69/3.67 cnf(ssp208, plain, (~spl1 | spl23 | spl194), inference(avatar_split_clause, [status(thm)], [p1627, sdef23, sdef194])).
% 24.69/3.67 cnf(p1629, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk2,line_connecting(sk0,sk1)) | apart_point_and_line(sk2,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(X3,sk3) | distinct_points(X3,X2) | ~spl1), inference(resolution, [status(thm)], [p177, p110])).
% 24.69/3.67 fof(sdef195, definition, (spl195 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | apart_point_and_line(sk2,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | distinct_points(X3,sk3) | distinct_points(X3,X2))), introduced(definition, [new_symbols(naming, [spl195])], [avatar_definition])).
% 24.69/3.67 cnf(ssp209, plain, (~spl1 | spl0 | spl195), inference(avatar_split_clause, [status(thm)], [p1629, sdef0, sdef195])).
% 24.69/3.67 cnf(p1632, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | distinct_points(X2,X3) | distinct_points(sk0,X4) | distinct_points(X2,X4) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X1) | apart_point_and_line(X3,line_connecting(sk0,sk1)) | apart_point_and_line(X3,X1) | ~spl1), inference(resolution, [status(thm)], [p177, p147])).
% 24.69/3.67 fof(sdef196, definition, (spl196 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | distinct_points(X2,X3) | distinct_points(sk0,X4) | distinct_points(X2,X4) | apart_point_and_line(sk1,X1) | apart_point_and_line(X3,line_connecting(sk0,sk1)) | apart_point_and_line(X3,X1))), introduced(definition, [new_symbols(naming, [spl196])], [avatar_definition])).
% 24.69/3.67 cnf(ssp210, plain, (~spl1 | spl23 | spl196), inference(avatar_split_clause, [status(thm)], [p1632, sdef23, sdef196])).
% 24.69/3.67 cnf(p1635, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | distinct_points(sk1,X2) | distinct_points(X3,X2) | distinct_points(X3,X4) | apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X1) | apart_point_and_line(X4,line_connecting(sk0,sk1)) | apart_point_and_line(X4,X1) | ~spl1), inference(resolution, [status(thm)], [p177, p149])).
% 24.69/3.67 fof(sdef197, definition, (spl197 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | distinct_points(sk1,X2) | distinct_points(X3,X2) | distinct_points(X3,X4) | apart_point_and_line(sk0,X1) | apart_point_and_line(X4,line_connecting(sk0,sk1)) | apart_point_and_line(X4,X1))), introduced(definition, [new_symbols(naming, [spl197])], [avatar_definition])).
% 24.69/3.67 cnf(ssp211, plain, (~spl1 | spl21 | spl197), inference(avatar_split_clause, [status(thm)], [p1635, sdef21, sdef197])).
% 24.69/3.67 cnf(p1638, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | distinct_points(X2,X3) | distinct_points(sk1,X4) | distinct_points(X3,X4) | apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1) | ~spl1), inference(resolution, [status(thm)], [p177, p169])).
% 24.69/3.67 fof(sdef198, definition, (spl198 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | distinct_points(X2,X3) | distinct_points(sk1,X4) | distinct_points(X3,X4) | apart_point_and_line(sk0,X1) | apart_point_and_line(X2,line_connecting(sk0,sk1)) | apart_point_and_line(X2,X1))), introduced(definition, [new_symbols(naming, [spl198])], [avatar_definition])).
% 24.69/3.67 cnf(ssp212, plain, (~spl1 | spl21 | spl198), inference(avatar_split_clause, [status(thm)], [p1638, sdef21, sdef198])).
% 24.69/3.67 cnf(p1640, plain, (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | distinct_points(sk0,X2) | distinct_points(X2,X3) | distinct_points(X3,X4) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X1) | apart_point_and_line(X4,line_connecting(sk0,sk1)) | apart_point_and_line(X4,X1) | ~spl1), inference(resolution, [status(thm)], [p177, p170])).
% 24.69/3.67 fof(sdef199, definition, (spl199 <=> (distinct_points(sk3,X0) | apart_point_and_line(X0,X1) | distinct_points(sk0,X2) | distinct_points(X2,X3) | distinct_points(X3,X4) | apart_point_and_line(sk1,X1) | apart_point_and_line(X4,line_connecting(sk0,sk1)) | apart_point_and_line(X4,X1))), introduced(definition, [new_symbols(naming, [spl199])], [avatar_definition])).
% 24.69/3.67 cnf(ssp213, plain, (~spl1 | spl23 | spl199), inference(avatar_split_clause, [status(thm)], [p1640, sdef23, sdef199])).
% 24.69/3.67 cnf(sat_ref, plain, $false, inference(avatar_sat_refutation, [status(thm)], [ssp0, ssp1, ssp2, ssp3, ssp4, ssp5, ssp6, ssp7, ssp8, ssp9, ssp10, ssp11, ssp12, ssp13, ssp14, ssp15, ssp16, ssp17, ssp18, ssp19, ssp20, ssp21, ssp22, ssp23, ssp24, ssp25, ssp26, ssp27, ssp28, ssp29, ssp30, ssp31, ssp32, ssp33, ssp34, ssp35, ssp36, ssp37, ssp38, ssp39, ssp40, ssp41, ssp42, ssp43, ssp44, ssp45, ssp46, ssp47, ssp48, ssp49, ssp50, ssp51, ssp52, ssp53, ssp54, ssp55, ssp56, ssp57, ssp58, ssp59, ssp60, ssp61, ssp62, ssp63, ssp64, ssp65, ssp66, ssp67, ssp68, ssp69, ssp70, ssp71, ssp72, ssp73, ssp74, ssp75, ssp76, ssp77, ssp78, ssp79, ssp80, ssp81, ssp82, ssp83, ssp84, ssp85, ssp86, ssp87, ssp88, ssp89, ssp90, ssp91, ssp92, ssp93, ssp94, ssp95, ssp96, ssp97, ssp98, ssp99, ssp100, ssp101, ssp102, ssp103, ssp104, ssp105, ssp106, ssp107, ssp108, ssp109, ssp110, ssp111, ssp112, ssp113, ssp114, ssp115, ssp116, ssp117, ssp118, ssp119, ssp120, ssp121, ssp122, ssp123, ssp124, ssp125, ssp126, ssp127, ssp128, ssp129, ssp130, ssp131, ssp132, ssp133, ssp134, ssp135, ssp136, ssp137, ssp138, ssp139, ssp140, ssp141, ssp142, ssp143, ssp144, ssp145, ssp146, ssp147, ssp148, ssp149, ssp150, ssp151, ssp152, ssp153, ssp154, ssp155, ssp156, ssp157, ssp158, ssp159, ssp160, ssp161, ssp162, ssp163, ssp164, ssp165, ssp166, ssp167, ssp168, ssp169, ssp170, ssp171, ssp172, ssp173, ssp174, ssp175, ssp176, ssp177, ssp178, ssp179, ssp180, ssp181, ssp182, ssp183, ssp184, ssp185, ssp186, ssp187, ssp188, ssp189, ssp190, ssp191, ssp192, ssp193, ssp194, ssp195, ssp196, ssp197, ssp198, ssp199, ssp200, ssp201, ssp202, ssp203, ssp204, ssp205, ssp206, ssp207, ssp208, ssp209, ssp210, ssp211, ssp212, ssp213, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8, sct9, sct10, sct11, sct12, sct13, sct14, sct15, sct16, sct17, sct18, sct19])).
% 24.69/3.67 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------