%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO204+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:17:28 PM UTC 2026
% Result : Theorem 22.81s 3.45s
% Output : Proof 22.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO204+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n006.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 11:27:56 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 22.81/3.45 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.81/3.45 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.81/3.45 fof(f3, axiom, ! [X,Y,Z] : ( distinct_points(X,Y) => ( distinct_points(X,Z) | distinct_points(Y,Z) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart4)).
% 22.81/3.45 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])).
% 22.81/3.45 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])).
% 22.81/3.45 cnf(c3, plain, ~distinct_points(X0,X1) | distinct_points(X0,X2) | distinct_points(X1,X2), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 22.81/3.45 fof(f12, conjecture, ! [X,Y,Z] : ( ( distinct_points(X,Y) & ~ distinct_points(Y,Z) ) => ( distinct_points(X,Z) & ~ distinct_lines(line_connecting(X,Y),line_connecting(X,Z)) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 22.81/3.45 fof(f12_neg, negated_conjecture, ~(! [X,Y,Z] : ( ( distinct_points(X,Y) & ~ distinct_points(Y,Z) ) => ( distinct_points(X,Z) & ~ distinct_lines(line_connecting(X,Y),line_connecting(X,Z)) ) )), inference(negated_conjecture, [status(cth)], [f12])).
% 22.81/3.45 fof(f12_nnf, plain, ? [X,Y,Z] : (((distinct_points(X,Y) & ~(distinct_points(Y,Z))) & (~(distinct_points(X,Z)) | distinct_lines(line_connecting(X,Y),line_connecting(X,Z))))), inference(nnf_transformation, [status(thm)], [f12_neg])).
% 22.81/3.45 fof(f12_sk, plain, ((distinct_points(sk0,sk1) & ~(distinct_points(sk1,sk2))) & (~(distinct_points(sk0,sk2)) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2])], [f12_nnf])).
% 22.81/3.45 cnf(c14, plain, distinct_points(sk0,sk1), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 22.81/3.45 cnf(p19, plain, distinct_points(sk0,X0) | distinct_points(sk1,X0), inference(resolution, [status(thm)], [c3, c14])).
% 22.81/3.45 cnf(c15, plain, ~distinct_points(sk1,sk2), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 22.81/3.45 cnf(p21, plain, distinct_points(sk0,sk2), inference(resolution, [status(thm)], [p19, c15])).
% 22.81/3.45 fof(sdef0, definition, (spl0 <=> (~distinct_points(sk0,sk2))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 22.81/3.45 cnf(p17, plain, (~distinct_points(sk0,sk2) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 22.81/3.45 cnf(p23, plain, ($false | ~spl0), inference(resolution, [status(thm)], [p21, p17])).
% 22.81/3.45 cnf(sct0, plain, (~spl0), inference(avatar_contradiction_clause, [status(thm)], [p23])).
% 22.81/3.45 fof(sdef2, definition, (spl2 <=> (apart_point_and_line(sk0,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 22.81/3.45 cnf(p547, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 22.81/3.45 fof(f6, axiom, ! [X,Y,Z] : ( distinct_points(X,Y) => ( apart_point_and_line(Z,line_connecting(X,Y)) => ( distinct_points(Z,X) & distinct_points(Z,Y) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con1)).
% 22.81/3.45 fof(f6_nnf, plain, ! [X,Y,Z] : ((~(distinct_points(X,Y)) | (~(apart_point_and_line(Z,line_connecting(X,Y))) | (distinct_points(Z,X) & distinct_points(Z,Y))))), inference(nnf_transformation, [status(thm)], [f6])).
% 22.81/3.45 fof(f6_sk, plain, ! [X,Y,Z] : ((~(distinct_points(X,Y)) | (~(apart_point_and_line(Z,line_connecting(X,Y))) | (distinct_points(Z,X) & distinct_points(Z,Y))))), inference(skolemisation, [status(esa)], [f6_nnf])).
% 22.81/3.45 cnf(c6, plain, ~distinct_points(X0,X1) | ~apart_point_and_line(X2,line_connecting(X0,X1)) | distinct_points(X2,X0), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 22.81/3.45 cnf(p37, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c6, c14])).
% 22.81/3.45 cnf(p574, plain, (distinct_points(sk0,sk0) | ~spl2), inference(resolution, [status(thm)], [p547, p37])).
% 22.81/3.45 fof(f0, axiom, ! [X] : ~ distinct_points(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart1)).
% 22.81/3.45 fof(f0_nnf, plain, ! [X] : (~(distinct_points(X,X))), inference(nnf_transformation, [status(thm)], [f0])).
% 22.81/3.45 fof(f0_sk, plain, ! [X] : (~(distinct_points(X,X))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 22.81/3.45 cnf(c0, plain, ~distinct_points(X0,X0), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.81/3.45 cnf(p577, plain, ($false | ~spl2), inference(resolution, [status(thm)], [p574, c0])).
% 22.81/3.45 cnf(sct1, plain, (~spl2), inference(avatar_contradiction_clause, [status(thm)], [p577])).
% 22.81/3.45 fof(sdef3, definition, (spl3 <=> (apart_point_and_line(sk0,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 22.81/3.45 cnf(p548, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 22.81/3.45 cnf(p39, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X0,sk0), inference(resolution, [status(thm)], [c6, p21])).
% 22.81/3.45 cnf(p578, plain, (distinct_points(sk0,sk0) | ~spl3), inference(resolution, [status(thm)], [p548, p39])).
% 22.81/3.45 cnf(p581, plain, ($false | ~spl3), inference(resolution, [status(thm)], [p578, c0])).
% 22.81/3.45 cnf(sct2, plain, (~spl3), inference(avatar_contradiction_clause, [status(thm)], [p581])).
% 22.81/3.45 fof(sdef4, definition, (spl4 <=> (apart_point_and_line(sk1,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 22.81/3.45 cnf(p549, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 22.81/3.45 cnf(c7, plain, ~distinct_points(X0,X1) | ~apart_point_and_line(X2,line_connecting(X0,X1)) | distinct_points(X2,X1), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 22.81/3.45 cnf(p61, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk1)) | distinct_points(X0,sk1), inference(resolution, [status(thm)], [c7, c14])).
% 22.81/3.45 cnf(p607, plain, (distinct_points(sk1,sk1) | ~spl4), inference(resolution, [status(thm)], [p549, p61])).
% 22.81/3.45 cnf(p610, plain, ($false | ~spl4), inference(resolution, [status(thm)], [p607, c0])).
% 22.81/3.45 cnf(sct3, plain, (~spl4), inference(avatar_contradiction_clause, [status(thm)], [p610])).
% 22.81/3.45 fof(sdef5, definition, (spl5 <=> (apart_point_and_line(sk1,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 22.81/3.45 cnf(p550, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 22.81/3.45 cnf(p63, plain, ~apart_point_and_line(X0,line_connecting(sk0,sk2)) | distinct_points(X0,sk2), inference(resolution, [status(thm)], [c7, p21])).
% 22.81/3.45 cnf(p611, plain, (distinct_points(sk1,sk2) | ~spl5), inference(resolution, [status(thm)], [p550, p63])).
% 22.81/3.45 cnf(p614, plain, ($false | ~spl5), inference(resolution, [status(thm)], [p611, c15])).
% 22.81/3.45 cnf(sct4, plain, (~spl5), inference(avatar_contradiction_clause, [status(thm)], [p614])).
% 22.81/3.45 cnf(c16, plain, ~distinct_points(sk0,sk2) | distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)), inference(cnf_transformation, [status(esa)], [f12_sk])).
% 22.81/3.45 fof(sdef1, definition, (spl1 <=> (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 22.81/3.45 cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [c16, sdef0, sdef1])).
% 22.81/3.45 fof(f8, axiom, ! [X,Y,U,V] : ( ( distinct_points(X,Y) & distinct_lines(U,V) ) => ( apart_point_and_line(X,U) | apart_point_and_line(X,V) | apart_point_and_line(Y,U) | apart_point_and_line(Y,V) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cu1)).
% 22.81/3.45 fof(f8_nnf, plain, ! [X,Y,U,V] : (((~(distinct_points(X,Y)) | ~(distinct_lines(U,V))) | (((apart_point_and_line(X,U) | apart_point_and_line(X,V)) | apart_point_and_line(Y,U)) | apart_point_and_line(Y,V)))), inference(nnf_transformation, [status(thm)], [f8])).
% 22.81/3.45 fof(f8_sk, plain, ! [X,Y,U,V] : (((~(distinct_points(X,Y)) | ~(distinct_lines(U,V))) | (((apart_point_and_line(X,U) | apart_point_and_line(X,V)) | apart_point_and_line(Y,U)) | apart_point_and_line(Y,V)))), inference(skolemisation, [status(esa)], [f8_nnf])).
% 22.81/3.45 cnf(c10, plain, ~distinct_points(X0,X1) | ~distinct_lines(X2,X3) | apart_point_and_line(X0,X2) | apart_point_and_line(X0,X3) | apart_point_and_line(X1,X2) | apart_point_and_line(X1,X3), inference(cnf_transformation, [status(esa)], [f8_sk])).
% 22.81/3.45 cnf(p109, 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])).
% 22.81/3.45 cnf(p18, plain, (distinct_lines(line_connecting(sk0,sk1),line_connecting(sk0,sk2)) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 22.81/3.45 cnf(p546, 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)) | ~spl1), inference(resolution, [status(thm)], [p109, p18])).
% 22.81/3.45 cnf(ssp1, plain, (~spl1 | spl2 | spl3 | spl4 | spl5), inference(avatar_split_clause, [status(thm)], [p546, sdef2, sdef3, sdef4, sdef5])).
% 22.81/3.45 fof(f4, axiom, ! [X,Y,Z] : ( distinct_lines(X,Y) => ( distinct_lines(X,Z) | distinct_lines(Y,Z) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart5)).
% 22.81/3.45 fof(f4_nnf, plain, ! [X,Y,Z] : ((~(distinct_lines(X,Y)) | (distinct_lines(X,Z) | distinct_lines(Y,Z)))), inference(nnf_transformation, [status(thm)], [f4])).
% 22.81/3.45 fof(f4_sk, plain, ! [X,Y,Z] : ((~(distinct_lines(X,Y)) | (distinct_lines(X,Z) | distinct_lines(Y,Z)))), inference(skolemisation, [status(esa)], [f4_nnf])).
% 22.81/3.45 cnf(c4, plain, ~distinct_lines(X0,X1) | distinct_lines(X0,X2) | distinct_lines(X1,X2), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 22.81/3.45 cnf(p20, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl1), inference(resolution, [status(thm)], [c4, p18])).
% 22.81/3.45 cnf(p551, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl1), inference(resolution, [status(thm)], [p109, p20])).
% 22.81/3.45 fof(sdef6, definition, (spl6 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 22.81/3.45 cnf(ssp2, plain, (~spl1 | spl3 | spl5 | spl6), inference(avatar_split_clause, [status(thm)], [p551, sdef3, sdef5, sdef6])).
% 22.81/3.45 cnf(p26, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X0,X1) | ~spl1), inference(resolution, [status(thm)], [p20, c4])).
% 22.81/3.45 cnf(p553, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X0,X1) | ~spl1), inference(resolution, [status(thm)], [p109, p26])).
% 22.81/3.45 fof(sdef7, definition, (spl7 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 22.81/3.45 cnf(ssp3, plain, (~spl1 | spl2 | spl4 | spl7), inference(avatar_split_clause, [status(thm)], [p553, sdef2, sdef4, sdef7])).
% 22.81/3.45 cnf(p555, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X1,X0) | ~spl1), inference(resolution, [status(thm)], [p109, p26])).
% 22.81/3.45 fof(sdef8, definition, (spl8 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 22.81/3.45 cnf(ssp4, plain, (~spl1 | spl3 | spl5 | spl8), inference(avatar_split_clause, [status(thm)], [p555, sdef3, sdef5, sdef8])).
% 22.81/3.45 cnf(p557, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(line_connecting(sk0,sk2),X1) | ~spl1), inference(resolution, [status(thm)], [p109, p26])).
% 22.81/3.45 fof(sdef9, definition, (spl9 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk2),X0))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 22.81/3.45 cnf(ssp5, plain, (~spl1 | spl6 | spl9), inference(avatar_split_clause, [status(thm)], [p557, sdef6, sdef9])).
% 22.81/3.45 fof(f1, axiom, ! [X] : ~ distinct_lines(X,X), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', apart2)).
% 22.81/3.45 fof(f1_nnf, plain, ! [X] : (~(distinct_lines(X,X))), inference(nnf_transformation, [status(thm)], [f1])).
% 22.81/3.45 fof(f1_sk, plain, ! [X] : (~(distinct_lines(X,X))), inference(skolemisation, [status(esa)], [f1_nnf])).
% 22.81/3.45 cnf(c1, plain, ~distinct_lines(X0,X0), inference(cnf_transformation, [status(esa)], [f1_sk])).
% 22.81/3.45 cnf(p167, plain, (distinct_lines(line_connecting(sk0,sk1),X0) | distinct_lines(X0,line_connecting(sk0,sk2)) | ~spl1), inference(resolution, [status(thm)], [p26, c1])).
% 22.81/3.45 cnf(p559, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | distinct_lines(X0,line_connecting(sk0,sk2)) | ~spl1), inference(resolution, [status(thm)], [p109, p167])).
% 22.81/3.45 fof(sdef10, definition, (spl10 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X0,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 22.81/3.45 cnf(ssp6, plain, (~spl1 | spl2 | spl4 | spl10), inference(avatar_split_clause, [status(thm)], [p559, sdef2, sdef4, sdef10])).
% 22.81/3.45 cnf(p171, plain, (distinct_lines(X0,line_connecting(sk0,sk2)) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X0,X1) | ~spl1), inference(resolution, [status(thm)], [p167, c4])).
% 22.81/3.45 cnf(p561, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X0,X1) | ~spl1), inference(resolution, [status(thm)], [p109, p171])).
% 22.81/3.45 fof(sdef11, definition, (spl11 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk1),X1) | distinct_lines(X0,X1))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 22.81/3.45 cnf(ssp7, plain, (~spl1 | spl3 | spl5 | spl11), inference(avatar_split_clause, [status(thm)], [p561, sdef3, sdef5, sdef11])).
% 22.81/3.45 cnf(p563, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | distinct_lines(X1,line_connecting(sk0,sk2)) | distinct_lines(X1,X0) | ~spl1), inference(resolution, [status(thm)], [p109, p171])).
% 22.81/3.45 fof(sdef12, definition, (spl12 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X1,line_connecting(sk0,sk2)) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 22.81/3.45 cnf(ssp8, plain, (~spl1 | spl2 | spl4 | spl12), inference(avatar_split_clause, [status(thm)], [p563, sdef2, sdef4, sdef12])).
% 22.81/3.45 cnf(p565, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X0,line_connecting(sk0,sk2)) | distinct_lines(line_connecting(sk0,sk1),X1) | ~spl1), inference(resolution, [status(thm)], [p109, p171])).
% 22.81/3.45 cnf(ssp9, plain, (~spl1 | spl6 | spl10), inference(avatar_split_clause, [status(thm)], [p565, sdef6, sdef10])).
% 22.81/3.45 cnf(p449, plain, (distinct_lines(X0,line_connecting(sk0,sk2)) | distinct_lines(X0,line_connecting(sk0,sk1)) | ~spl1), inference(resolution, [status(thm)], [p171, c1])).
% 22.81/3.45 cnf(p566, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | distinct_lines(X0,line_connecting(sk0,sk1)) | ~spl1), inference(resolution, [status(thm)], [p109, p449])).
% 22.81/3.45 fof(sdef13, definition, (spl13 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X0,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 22.81/3.45 cnf(ssp10, plain, (~spl1 | spl3 | spl5 | spl13), inference(avatar_split_clause, [status(thm)], [p566, sdef3, sdef5, sdef13])).
% 22.81/3.45 cnf(p453, plain, (distinct_lines(X0,line_connecting(sk0,sk1)) | distinct_lines(X0,X1) | distinct_lines(line_connecting(sk0,sk2),X1) | ~spl1), inference(resolution, [status(thm)], [p449, c4])).
% 22.81/3.45 cnf(p568, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | distinct_lines(X0,line_connecting(sk0,sk1)) | distinct_lines(line_connecting(sk0,sk2),X1) | ~spl1), inference(resolution, [status(thm)], [p109, p453])).
% 22.81/3.45 cnf(ssp11, plain, (~spl1 | spl9 | spl13), inference(avatar_split_clause, [status(thm)], [p568, sdef9, sdef13])).
% 22.81/3.45 cnf(p569, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk2)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | distinct_lines(X1,line_connecting(sk0,sk1)) | distinct_lines(X1,X0) | ~spl1), inference(resolution, [status(thm)], [p109, p453])).
% 22.81/3.45 fof(sdef14, definition, (spl14 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(X1,line_connecting(sk0,sk1)) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 22.81/3.45 cnf(ssp12, plain, (~spl1 | spl3 | spl5 | spl14), inference(avatar_split_clause, [status(thm)], [p569, sdef3, sdef5, sdef14])).
% 22.81/3.45 cnf(p527, plain, (distinct_lines(X0,line_connecting(sk0,sk1)) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl1), inference(resolution, [status(thm)], [p453, c1])).
% 22.81/3.45 cnf(p571, plain, (apart_point_and_line(sk0,X0) | apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl1), inference(resolution, [status(thm)], [p109, p527])).
% 22.81/3.45 cnf(ssp13, plain, (~spl1 | spl2 | spl4 | spl9), inference(avatar_split_clause, [status(thm)], [p571, sdef2, sdef4, sdef9])).
% 22.81/3.45 cnf(p530, plain, (distinct_lines(line_connecting(sk0,sk2),X0) | distinct_lines(X0,X1) | distinct_lines(line_connecting(sk0,sk1),X1) | ~spl1), inference(resolution, [status(thm)], [p527, c4])).
% 22.81/3.45 cnf(p572, plain, (apart_point_and_line(sk0,line_connecting(sk0,sk1)) | apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0) | ~spl1), inference(resolution, [status(thm)], [p109, p530])).
% 22.81/3.45 fof(sdef15, definition, (spl15 <=> (apart_point_and_line(sk0,X0) | apart_point_and_line(sk1,X0) | distinct_lines(line_connecting(sk0,sk2),X1) | distinct_lines(X1,X0))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 22.81/3.45 cnf(ssp14, plain, (~spl1 | spl2 | spl4 | spl15), inference(avatar_split_clause, [status(thm)], [p572, sdef2, sdef4, sdef15])).
% 22.81/3.45 cnf(p110, plain, ~distinct_lines(X0,X1) | apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,X1) | apart_point_and_line(X2,X0) | apart_point_and_line(X2,X1) | distinct_points(sk0,X2), inference(resolution, [status(thm)], [c10, p19])).
% 22.81/3.45 cnf(p582, 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) | ~spl1), inference(resolution, [status(thm)], [p110, p18])).
% 22.81/3.45 fof(sdef16, definition, (spl16 <=> (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, [spl16])], [avatar_definition])).
% 22.81/3.45 cnf(ssp15, plain, (~spl1 | spl4 | spl5 | spl16), inference(avatar_split_clause, [status(thm)], [p582, sdef4, sdef5, sdef16])).
% 22.81/3.45 cnf(p584, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X0) | ~spl1), inference(resolution, [status(thm)], [p110, p20])).
% 22.81/3.45 fof(sdef17, definition, (spl17 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X0))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 22.81/3.45 cnf(ssp16, plain, (~spl1 | spl5 | spl17), inference(avatar_split_clause, [status(thm)], [p584, sdef5, sdef17])).
% 22.81/3.45 cnf(p586, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X0,X2) | ~spl1), inference(resolution, [status(thm)], [p110, p26])).
% 22.81/3.45 fof(sdef18, definition, (spl18 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 22.81/3.45 cnf(ssp17, plain, (~spl1 | spl4 | spl18), inference(avatar_split_clause, [status(thm)], [p586, sdef4, sdef18])).
% 22.81/3.45 cnf(p588, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X2) | distinct_lines(X2,X0) | ~spl1), inference(resolution, [status(thm)], [p110, p26])).
% 22.81/3.45 fof(sdef19, definition, (spl19 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 22.81/3.45 cnf(ssp18, plain, (~spl1 | spl5 | spl19), inference(avatar_split_clause, [status(thm)], [p588, sdef5, sdef19])).
% 22.81/3.45 cnf(p591, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk0,sk2)) | ~spl1), inference(resolution, [status(thm)], [p110, p167])).
% 22.81/3.45 fof(sdef20, definition, (spl20 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk0,sk2)))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 22.81/3.45 cnf(ssp19, plain, (~spl1 | spl4 | spl20), inference(avatar_split_clause, [status(thm)], [p591, sdef4, sdef20])).
% 22.81/3.45 cnf(p593, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X2) | distinct_lines(X0,X2) | ~spl1), inference(resolution, [status(thm)], [p110, p171])).
% 22.81/3.45 fof(sdef21, definition, (spl21 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk1),X2) | distinct_lines(X0,X2))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 22.81/3.45 cnf(ssp20, plain, (~spl1 | spl5 | spl21), inference(avatar_split_clause, [status(thm)], [p593, sdef5, sdef21])).
% 22.81/3.45 cnf(p595, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,line_connecting(sk0,sk2)) | distinct_lines(X2,X0) | ~spl1), inference(resolution, [status(thm)], [p110, p171])).
% 22.81/3.45 fof(sdef22, definition, (spl22 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,line_connecting(sk0,sk2)) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 22.81/3.45 cnf(ssp21, plain, (~spl1 | spl4 | spl22), inference(avatar_split_clause, [status(thm)], [p595, sdef4, sdef22])).
% 22.81/3.45 cnf(p598, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk0,sk1)) | ~spl1), inference(resolution, [status(thm)], [p110, p449])).
% 22.81/3.45 fof(sdef23, definition, (spl23 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | distinct_points(sk0,X1) | distinct_lines(X0,line_connecting(sk0,sk1)))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 22.81/3.45 cnf(ssp22, plain, (~spl1 | spl5 | spl23), inference(avatar_split_clause, [status(thm)], [p598, sdef5, sdef23])).
% 22.81/3.45 cnf(p601, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk2)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,line_connecting(sk0,sk1)) | distinct_lines(X2,X0) | ~spl1), inference(resolution, [status(thm)], [p110, p453])).
% 22.81/3.45 fof(sdef24, definition, (spl24 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk2)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(X2,line_connecting(sk0,sk1)) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 22.81/3.45 cnf(ssp23, plain, (~spl1 | spl5 | spl24), inference(avatar_split_clause, [status(thm)], [p601, sdef5, sdef24])).
% 22.81/3.45 cnf(p603, plain, (apart_point_and_line(sk1,X0) | apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X0) | ~spl1), inference(resolution, [status(thm)], [p110, p527])).
% 22.81/3.45 fof(sdef25, definition, (spl25 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X0))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 22.81/3.45 cnf(ssp24, plain, (~spl1 | spl4 | spl25), inference(avatar_split_clause, [status(thm)], [p603, sdef4, sdef25])).
% 22.81/3.45 cnf(p605, plain, (apart_point_and_line(sk1,line_connecting(sk0,sk1)) | apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X2,X0) | ~spl1), inference(resolution, [status(thm)], [p110, p530])).
% 22.81/3.45 fof(sdef26, definition, (spl26 <=> (apart_point_and_line(sk1,X0) | apart_point_and_line(X1,line_connecting(sk0,sk1)) | apart_point_and_line(X1,X0) | distinct_points(sk0,X1) | distinct_lines(line_connecting(sk0,sk2),X2) | distinct_lines(X2,X0))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 22.81/3.45 cnf(ssp25, plain, (~spl1 | spl4 | spl26), inference(avatar_split_clause, [status(thm)], [p605, sdef4, sdef26])).
% 22.81/3.45 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, sct0, sct1, sct2, sct3, sct4])).
% 22.81/3.45 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------