%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO077-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 : Thu Sep 24 12:25:42 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO077-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.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 : Sun Sep 20 09:59:26 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.53 % Refutation found
% 0.09/0.53 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.53 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.53 fof(f1,axiom,(
% 0.09/0.53 (![Z1,Z2]: (( on(Z1,line_from_to(Z1,Z2))| Z1 = Z2| ~ point(Z1)| ~ point(Z2) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f2,axiom,(
% 0.09/0.53 (![Z2,Z1]: (( on(Z2,line_from_to(Z1,Z2))| Z1 = Z2| ~ point(Z1)| ~ point(Z2) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f3,axiom,(
% 0.09/0.53 (![Z1,Z2]: (( line(line_from_to(Z1,Z2))| Z1 = Z2| ~ point(Z1)| ~ point(Z2) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f4,axiom,(
% 0.09/0.53 (![Z1,Y3,Z2,Y4]: (( ~ on(Z1,Y3)| Z1 = Z2| ~ on(Z2,Y3)| Y3 = Y4| ~ on(Z1,Y4)| ~ on(Z2,Y4)| ~ point(Z1)| ~ point(Z2)| ~ line(Y3)| ~ line(Y4) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f27,axiom,(
% 0.09/0.53 (![X1,X2,X3]: (( ~ point(X1)| ~ point(X2)| ~ point(X3)| X1 = X2| X1 = X3| X2 = X3| on(X1,line_through_3_points(X1,X2,X3))| ~ collinear(X1,X2,X3) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f28,axiom,(
% 0.09/0.53 (![X1,X2,X3]: (( ~ point(X1)| ~ point(X2)| ~ point(X3)| X1 = X2| X1 = X3| X2 = X3| on(X2,line_through_3_points(X1,X2,X3))| ~ collinear(X1,X2,X3) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f29,axiom,(
% 0.09/0.53 (![X1,X2,X3]: (( ~ point(X1)| ~ point(X2)| ~ point(X3)| X1 = X2| X1 = X3| X2 = X3| on(X3,line_through_3_points(X1,X2,X3))| ~ collinear(X1,X2,X3) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f30,axiom,(
% 0.09/0.53 (![X1,X2,X3]: (( ~ point(X1)| ~ point(X2)| ~ point(X3)| X1 = X2| X1 = X3| X2 = X3| line(line_through_3_points(X1,X2,X3))| ~ collinear(X1,X2,X3) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f32,hypothesis,(
% 0.09/0.53 point(point1) ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f33,hypothesis,(
% 0.09/0.53 point(point2) ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f34,hypothesis,(
% 0.09/0.53 point(point3) ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f35,hypothesis,(
% 0.09/0.53 line(a_line) ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f36,hypothesis,(
% 0.09/0.53 on(point1,a_line) ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f37,hypothesis,(
% 0.09/0.53 on(point2,a_line) ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f38,hypothesis,(
% 0.09/0.53 ~ on(point3,a_line) ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f39,hypothesis,(
% 0.09/0.53 point1 != point2 ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f40,hypothesis,(
% 0.09/0.53 point1 != point3 ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f41,hypothesis,(
% 0.09/0.53 point2 != point3 ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f42,negated_conjecture,(
% 0.09/0.53 collinear(point1,point2,point3) ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f43,plain,(
% 0.09/0.53 ![Z2]: ((![Z1]: ((on(Z1,line_from_to(Z1,Z2))|Z1=Z2)|~point(Z1)))|~point(Z2))),
% 0.09/0.53 inference(miniscoping,[status(thm)],[f1])).
% 0.09/0.53 fof(f44,plain,(
% 0.09/0.53 ![X0,X1]: (on(X0,line_from_to(X0,X1))|X0=X1|~point(X0)|~point(X1))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f43])).
% 0.09/0.53 fof(f45,plain,(
% 0.09/0.53 ![Z2]: ((![Z1]: ((on(Z2,line_from_to(Z1,Z2))|Z1=Z2)|~point(Z1)))|~point(Z2))),
% 0.09/0.53 inference(miniscoping,[status(thm)],[f2])).
% 0.09/0.53 fof(f46,plain,(
% 0.09/0.53 ![X0,X1]: (on(X0,line_from_to(X1,X0))|X1=X0|~point(X1)|~point(X0))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f45])).
% 0.09/0.53 fof(f47,plain,(
% 0.09/0.53 ![Z2]: ((![Z1]: ((line(line_from_to(Z1,Z2))|Z1=Z2)|~point(Z1)))|~point(Z2))),
% 0.09/0.53 inference(miniscoping,[status(thm)],[f3])).
% 0.09/0.53 fof(f48,plain,(
% 0.09/0.53 ![X0,X1]: (line(line_from_to(X0,X1))|X0=X1|~point(X0)|~point(X1))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f47])).
% 0.09/0.53 fof(f49,plain,(
% 0.09/0.53 ![Y4]: ((![Y3]: ((![Z2]: ((![Z1]: ((((((~on(Z1,Y3)|Z1=Z2)|~on(Z2,Y3))|Y3=Y4)|~on(Z1,Y4))|~on(Z2,Y4))|~point(Z1)))|~point(Z2)))|~line(Y3)))|~line(Y4))),
% 0.09/0.53 inference(miniscoping,[status(thm)],[f4])).
% 0.09/0.53 fof(f50,plain,(
% 0.09/0.53 ![X0,X1,X2,X3]: (~on(X0,X1)|X0=X2|~on(X2,X1)|X1=X3|~on(X0,X3)|~on(X2,X3)|~point(X0)|~point(X2)|~line(X1)|~line(X3))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f49])).
% 0.09/0.53 fof(f79,plain,(
% 0.09/0.53 ![X0,X1,X2]: (~point(X0)|~point(X1)|~point(X2)|X0=X1|X0=X2|X1=X2|on(X0,line_through_3_points(X0,X1,X2))|~collinear(X0,X1,X2))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f27])).
% 0.09/0.53 fof(f80,plain,(
% 0.09/0.53 ![X0,X1,X2]: (~point(X0)|~point(X1)|~point(X2)|X0=X1|X0=X2|X1=X2|on(X1,line_through_3_points(X0,X1,X2))|~collinear(X0,X1,X2))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f28])).
% 0.09/0.53 fof(f81,plain,(
% 0.09/0.53 ![X0,X1,X2]: (~point(X0)|~point(X1)|~point(X2)|X0=X1|X0=X2|X1=X2|on(X2,line_through_3_points(X0,X1,X2))|~collinear(X0,X1,X2))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f29])).
% 0.09/0.53 fof(f82,plain,(
% 0.09/0.53 ![X0,X1,X2]: (~point(X0)|~point(X1)|~point(X2)|X0=X1|X0=X2|X1=X2|line(line_through_3_points(X0,X1,X2))|~collinear(X0,X1,X2))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f30])).
% 0.09/0.53 fof(f85,plain,(
% 0.09/0.53 point(point1)),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f32])).
% 0.09/0.53 fof(f86,plain,(
% 0.09/0.53 point(point2)),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f33])).
% 0.09/0.53 fof(f87,plain,(
% 0.09/0.53 point(point3)),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f34])).
% 0.09/0.53 fof(f88,plain,(
% 0.09/0.53 line(a_line)),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f35])).
% 0.09/0.53 fof(f89,plain,(
% 0.09/0.53 on(point1,a_line)),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f36])).
% 0.09/0.53 fof(f90,plain,(
% 0.09/0.53 on(point2,a_line)),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f37])).
% 0.09/0.53 fof(f91,plain,(
% 0.09/0.53 ~on(point3,a_line)),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f38])).
% 0.09/0.53 fof(f92,plain,(
% 0.09/0.53 ~point1=point2),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f39])).
% 0.09/0.53 fof(f93,plain,(
% 0.09/0.53 ~point1=point3),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f40])).
% 0.09/0.53 fof(f94,plain,(
% 0.09/0.53 ~point2=point3),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f41])).
% 0.09/0.53 fof(f95,plain,(
% 0.09/0.53 collinear(point1,point2,point3)),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f42])).
% 0.09/0.53 fof(f112,definition,(
% 0.09/0.53 sQ1_spl <=> (point(point1))),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f114,plain,(
% 0.09/0.53 ~point(point1)|sQ1_spl),
% 0.09/0.53 inference(component_clause,[status(thm)],[f112])).
% 0.09/0.53 fof(f115,definition,(
% 0.09/0.53 sQ2_spl <=> (line(a_line))),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f117,plain,(
% 0.09/0.53 ~line(a_line)|sQ2_spl),
% 0.09/0.53 inference(component_clause,[status(thm)],[f115])).
% 0.09/0.53 fof(f119,plain,(
% 0.09/0.53 $false|sQ2_spl),
% 0.09/0.53 inference(forward_subsumption_resolution,[status(thm)],[f117,f88])).
% 0.09/0.53 fof(f120,plain,(
% 0.09/0.53 sQ2_spl),
% 0.09/0.53 inference(contradiction_clause,[status(thm)],[f119])).
% 0.09/0.53 fof(f129,plain,(
% 0.09/0.53 $false|sQ1_spl),
% 0.09/0.53 inference(forward_subsumption_resolution,[status(thm)],[f114,f85])).
% 0.09/0.53 fof(f130,plain,(
% 0.09/0.53 sQ1_spl),
% 0.09/0.53 inference(contradiction_clause,[status(thm)],[f129])).
% 0.09/0.53 fof(f148,plain,(
% 0.09/0.53 ![X0]: (on(point2,line_from_to(point2,X0))|point2=X0|~point(X0))),
% 0.09/0.53 inference(resolution,[status(thm)],[f44,f86])).
% 0.09/0.53 fof(f163,definition,(
% 0.09/0.53 sQ11_spl <=> (point3=point2)),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f164,plain,(
% 0.09/0.53 point3=point2|~sQ11_spl),
% 0.09/0.53 inference(component_clause,[status(thm)],[f163])).
% 0.09/0.53 fof(f170,definition,(
% 0.09/0.53 sQ13_spl <=> (point3=point1)),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f171,plain,(
% 0.09/0.53 point3=point1|~sQ13_spl),
% 0.09/0.53 inference(component_clause,[status(thm)],[f170])).
% 0.09/0.53 fof(f176,plain,(
% 0.09/0.53 on(point2,line_from_to(point2,point1))|point2=point1),
% 0.09/0.53 inference(resolution,[status(thm)],[f148,f85])).
% 0.09/0.53 fof(f188,definition,(
% 0.09/0.53 sQ17_spl <=> (on(point2,line_from_to(point2,point1)))),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f189,plain,(
% 0.09/0.53 on(point2,line_from_to(point2,point1))|~sQ17_spl),
% 0.09/0.53 inference(component_clause,[status(thm)],[f188])).
% 0.09/0.53 fof(f191,definition,(
% 0.09/0.53 sQ18_spl <=> (point2=point1)),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f192,plain,(
% 0.09/0.53 point2=point1|~sQ18_spl),
% 0.09/0.53 inference(component_clause,[status(thm)],[f191])).
% 0.09/0.53 fof(f194,plain,(
% 0.09/0.53 sQ17_spl|sQ18_spl),
% 0.09/0.53 inference(split_clause,[status(thm)],[f176,f188,f191])).
% 0.09/0.53 fof(f195,plain,(
% 0.09/0.53 $false|~sQ11_spl),
% 0.09/0.53 inference(forward_subsumption_resolution,[status(thm)],[f164,f94])).
% 0.09/0.53 fof(f196,plain,(
% 0.09/0.53 ~sQ11_spl),
% 0.09/0.53 inference(contradiction_clause,[status(thm)],[f195])).
% 0.09/0.53 fof(f212,plain,(
% 0.09/0.53 $false|~sQ18_spl),
% 0.09/0.53 inference(forward_subsumption_resolution,[status(thm)],[f192,f92])).
% 0.09/0.53 fof(f213,plain,(
% 0.09/0.53 ~sQ18_spl),
% 0.09/0.53 inference(contradiction_clause,[status(thm)],[f212])).
% 0.09/0.53 fof(f214,plain,(
% 0.09/0.53 $false|~sQ13_spl),
% 0.09/0.53 inference(forward_subsumption_resolution,[status(thm)],[f171,f93])).
% 0.09/0.53 fof(f215,plain,(
% 0.09/0.53 ~sQ13_spl),
% 0.09/0.53 inference(contradiction_clause,[status(thm)],[f214])).
% 0.09/0.53 fof(f217,plain,(
% 0.09/0.53 ![X0]: (on(X0,line_from_to(point2,X0))|point2=X0|~point(X0))),
% 0.09/0.53 inference(resolution,[status(thm)],[f46,f86])).
% 0.09/0.53 fof(f233,plain,(
% 0.09/0.53 on(point1,line_from_to(point2,point1))|point2=point1),
% 0.09/0.53 inference(resolution,[status(thm)],[f217,f85])).
% 0.09/0.53 fof(f239,definition,(
% 0.09/0.53 sQ25_spl <=> (on(point1,line_from_to(point2,point1)))),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f242,plain,(
% 0.09/0.53 sQ25_spl|sQ18_spl),
% 0.09/0.53 inference(split_clause,[status(thm)],[f233,f239,f191])).
% 0.09/0.53 fof(f256,plain,(
% 0.09/0.53 ![X0]: (line(line_from_to(point2,X0))|point2=X0|~point(X0))),
% 0.09/0.53 inference(resolution,[status(thm)],[f48,f86])).
% 0.09/0.53 fof(f275,plain,(
% 0.09/0.53 line(line_from_to(point2,point1))|point2=point1),
% 0.09/0.53 inference(resolution,[status(thm)],[f256,f85])).
% 0.09/0.53 fof(f284,definition,(
% 0.09/0.53 sQ33_spl <=> (line(line_from_to(point2,point1)))),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f287,plain,(
% 0.09/0.53 sQ33_spl|sQ18_spl),
% 0.09/0.53 inference(split_clause,[status(thm)],[f275,f284,f191])).
% 0.09/0.53 fof(f613,plain,(
% 0.09/0.53 ~point(point1)|~point(point2)|~point(point3)|point1=point2|point1=point3|point2=point3|line(line_through_3_points(point1,point2,point3))),
% 0.09/0.53 inference(resolution,[status(thm)],[f82,f95])).
% 0.09/0.53 fof(f614,definition,(
% 0.09/0.53 sQ105_spl <=> (point(point2))),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f616,plain,(
% 0.09/0.54 ~point(point2)|sQ105_spl),
% 0.09/0.54 inference(component_clause,[status(thm)],[f614])).
% 0.09/0.54 fof(f617,definition,(
% 0.09/0.54 sQ106_spl <=> (point(point3))),
% 0.09/0.54 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.09/0.54 fof(f619,plain,(
% 0.09/0.54 ~point(point3)|sQ106_spl),
% 0.09/0.54 inference(component_clause,[status(thm)],[f617])).
% 0.09/0.54 fof(f620,definition,(
% 0.09/0.54 sQ107_spl <=> (line(line_through_3_points(point1,point2,point3)))),
% 0.09/0.54 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.09/0.54 fof(f623,plain,(
% 0.09/0.54 ~sQ1_spl|~sQ105_spl|~sQ106_spl|sQ18_spl|sQ13_spl|sQ11_spl|sQ107_spl),
% 0.09/0.54 inference(split_clause,[status(thm)],[f613,f112,f614,f617,f191,f170,f163,f620])).
% 0.09/0.54 fof(f675,plain,(
% 0.09/0.54 ~point(point1)|~point(point2)|~point(point3)|point1=point2|point1=point3|point2=point3|on(point1,line_through_3_points(point1,point2,point3))),
% 0.09/0.54 inference(resolution,[status(thm)],[f79,f95])).
% 0.09/0.54 fof(f676,definition,(
% 0.09/0.54 sQ117_spl <=> (on(point1,line_through_3_points(point1,point2,point3)))),
% 0.09/0.54 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.09/0.54 fof(f677,plain,(
% 0.09/0.54 on(point1,line_through_3_points(point1,point2,point3))|~sQ117_spl),
% 0.09/0.54 inference(component_clause,[status(thm)],[f676])).
% 0.09/0.54 fof(f679,plain,(
% 0.09/0.54 ~sQ1_spl|~sQ105_spl|~sQ106_spl|sQ18_spl|sQ13_spl|sQ11_spl|sQ117_spl),
% 0.09/0.54 inference(split_clause,[status(thm)],[f675,f112,f614,f617,f191,f170,f163,f676])).
% 0.09/0.54 fof(f680,plain,(
% 0.09/0.54 $false|sQ106_spl),
% 0.09/0.54 inference(forward_subsumption_resolution,[status(thm)],[f619,f87])).
% 0.09/0.54 fof(f681,plain,(
% 0.09/0.54 sQ106_spl),
% 0.09/0.54 inference(contradiction_clause,[status(thm)],[f680])).
% 0.09/0.54 fof(f682,plain,(
% 0.09/0.54 $false|sQ105_spl),
% 0.09/0.54 inference(forward_subsumption_resolution,[status(thm)],[f616,f86])).
% 0.09/0.54 fof(f683,plain,(
% 0.09/0.54 sQ105_spl),
% 0.09/0.54 inference(contradiction_clause,[status(thm)],[f682])).
% 0.09/0.54 fof(f684,plain,(
% 0.09/0.54 ~point(point1)|~point(point2)|~point(point3)|point1=point2|point1=point3|point2=point3|on(point2,line_through_3_points(point1,point2,point3))),
% 0.09/0.54 inference(resolution,[status(thm)],[f80,f95])).
% 0.09/0.54 fof(f685,definition,(
% 0.09/0.54 sQ118_spl <=> (on(point2,line_through_3_points(point1,point2,point3)))),
% 0.09/0.54 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.09/0.54 fof(f686,plain,(
% 0.09/0.54 on(point2,line_through_3_points(point1,point2,point3))|~sQ118_spl),
% 0.09/0.54 inference(component_clause,[status(thm)],[f685])).
% 0.09/0.54 fof(f688,plain,(
% 0.09/0.54 ~sQ1_spl|~sQ105_spl|~sQ106_spl|sQ18_spl|sQ13_spl|sQ11_spl|sQ118_spl),
% 0.09/0.54 inference(split_clause,[status(thm)],[f684,f112,f614,f617,f191,f170,f163,f685])).
% 0.09/0.54 fof(f689,plain,(
% 0.09/0.54 ~point(point1)|~point(point2)|~point(point3)|point1=point2|point1=point3|point2=point3|on(point3,line_through_3_points(point1,point2,point3))),
% 0.09/0.54 inference(resolution,[status(thm)],[f81,f95])).
% 0.09/0.54 fof(f690,definition,(
% 0.09/0.54 sQ119_spl <=> (on(point3,line_through_3_points(point1,point2,point3)))),
% 0.09/0.54 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.09/0.54 fof(f691,plain,(
% 0.09/0.54 on(point3,line_through_3_points(point1,point2,point3))|~sQ119_spl),
% 0.09/0.54 inference(component_clause,[status(thm)],[f690])).
% 0.09/0.54 fof(f693,plain,(
% 0.09/0.54 ~sQ1_spl|~sQ105_spl|~sQ106_spl|sQ18_spl|sQ13_spl|sQ11_spl|sQ119_spl),
% 0.09/0.54 inference(split_clause,[status(thm)],[f689,f112,f614,f617,f191,f170,f163,f690])).
% 0.09/0.54 fof(f938,plain,(
% 0.09/0.54 ![X0,X1]: (point1=X0|~on(X0,line_through_3_points(point1,point2,point3))|line_through_3_points(point1,point2,point3)=X1|~on(point1,X1)|~on(X0,X1)|~point(point1)|~point(X0)|~line(line_through_3_points(point1,point2,point3))|~line(X1)|~sQ117_spl)),
% 0.09/0.54 inference(resolution,[status(thm)],[f677,f50])).
% 0.09/0.54 fof(f957,definition,(
% 0.09/0.54 ![X0,X1]: (sQ165_spl <=> (point1=X0|~on(X0,line_through_3_points(point1,point2,point3))|line_through_3_points(point1,point2,point3)=X1|~on(point1,X1)|~on(X0,X1)|~point(X0)|~line(X1)))),
% 0.09/0.54 introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition])).
% 0.09/0.54 fof(f958,plain,(
% 0.09/0.54 ![X0,X1]: (point1=X0|~on(X0,line_through_3_points(point1,point2,point3))|line_through_3_points(point1,point2,point3)=X1|~on(point1,X1)|~on(X0,X1)|~point(X0)|~line(X1)|~sQ165_spl)),
% 0.09/0.54 inference(component_clause,[status(thm)],[f957])).
% 0.09/0.54 fof(f960,plain,(
% 0.09/0.54 sQ165_spl|~sQ1_spl|~sQ107_spl|~sQ117_spl),
% 0.09/0.54 inference(split_clause,[status(thm)],[f938,f957,f112,f620,f676])).
% 0.09/0.54 fof(f983,plain,(
% 0.09/0.54 ![X0]: (point1=point2|line_through_3_points(point1,point2,point3)=X0|~on(point1,X0)|~on(point2,X0)|~point(point2)|~line(X0)|~sQ118_spl|~sQ165_spl)),
% 0.09/0.54 inference(resolution,[status(thm)],[f686,f958])).
% 0.09/0.54 fof(f992,definition,(
% 0.09/0.54 ![X0]: (sQ171_spl <=> (line_through_3_points(point1,point2,point3)=X0|~on(point1,X0)|~on(point2,X0)|~line(X0)))),
% 0.09/0.54 introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition])).
% 0.09/0.54 fof(f993,plain,(
% 0.09/0.54 ![X0]: (line_through_3_points(point1,point2,point3)=X0|~on(point1,X0)|~on(point2,X0)|~line(X0)|~sQ171_spl)),
% 0.09/0.54 inference(component_clause,[status(thm)],[f992])).
% 0.09/0.54 fof(f995,plain,(
% 0.09/0.54 sQ18_spl|sQ171_spl|~sQ105_spl|~sQ118_spl|~sQ165_spl),
% 0.09/0.54 inference(split_clause,[status(thm)],[f983,f191,f992,f614,f685,f957])).
% 0.09/0.54 fof(f3942,plain,(
% 0.09/0.54 line_through_3_points(point1,point2,point3)=a_line|~on(point1,a_line)|~line(a_line)|~sQ171_spl),
% 0.09/0.54 inference(resolution,[status(thm)],[f993,f90])).
% 0.09/0.54 fof(f3943,plain,(
% 0.09/0.54 line_through_3_points(point1,point2,point3)=line_from_to(point2,point1)|~on(point1,line_from_to(point2,point1))|~line(line_from_to(point2,point1))|~sQ171_spl|~sQ17_spl),
% 0.09/0.54 inference(resolution,[status(thm)],[f993,f189])).
% 0.09/0.54 fof(f3946,definition,(
% 0.09/0.54 sQ639_spl <=> (line_through_3_points(point1,point2,point3)=a_line)),
% 0.09/0.54 introduced(definition,[new_symbols(definition,[sQ639_spl])],[split_symbol_definition])).
% 0.09/0.54 fof(f3947,plain,(
% 0.09/0.54 line_through_3_points(point1,point2,point3)=a_line|~sQ639_spl),
% 0.09/0.54 inference(component_clause,[status(thm)],[f3946])).
% 0.09/0.54 fof(f3949,definition,(
% 0.09/0.54 sQ640_spl <=> (on(point1,a_line))),
% 0.09/0.54 introduced(definition,[new_symbols(definition,[sQ640_spl])],[split_symbol_definition])).
% 0.09/0.54 fof(f3951,plain,(
% 0.09/0.54 ~on(point1,a_line)|sQ640_spl),
% 0.09/0.54 inference(component_clause,[status(thm)],[f3949])).
% 0.09/0.54 fof(f3952,plain,(
% 0.09/0.54 sQ639_spl|~sQ640_spl|~sQ2_spl|~sQ171_spl),
% 0.09/0.54 inference(split_clause,[status(thm)],[f3942,f3946,f3949,f115,f992])).
% 0.09/0.54 fof(f3953,definition,(
% 0.09/0.55 sQ641_spl <=> (line_through_3_points(point1,point2,point3)=line_from_to(point2,point1))),
% 0.09/0.55 introduced(definition,[new_symbols(definition,[sQ641_spl])],[split_symbol_definition])).
% 0.09/0.55 fof(f3954,plain,(
% 0.09/0.55 line_through_3_points(point1,point2,point3)=line_from_to(point2,point1)|~sQ641_spl),
% 0.09/0.55 inference(component_clause,[status(thm)],[f3953])).
% 0.09/0.55 fof(f3956,plain,(
% 0.09/0.55 sQ641_spl|~sQ25_spl|~sQ33_spl|~sQ171_spl|~sQ17_spl),
% 0.09/0.55 inference(split_clause,[status(thm)],[f3943,f3953,f239,f284,f992,f188])).
% 0.09/0.55 fof(f4009,plain,(
% 0.09/0.55 on(point3,line_from_to(point2,point1))|~sQ641_spl|~sQ119_spl),
% 0.09/0.55 inference(backward_demodulation,[status(thm)],[f3954,f691])).
% 0.09/0.55 fof(f4075,plain,(
% 0.09/0.55 a_line=line_from_to(point2,point1)|~sQ639_spl|~sQ641_spl),
% 0.09/0.55 inference(backward_demodulation,[status(thm)],[f3947,f3954])).
% 0.09/0.55 fof(f4222,plain,(
% 0.09/0.55 on(point3,a_line)|~sQ639_spl|~sQ641_spl|~sQ119_spl),
% 0.09/0.55 inference(backward_demodulation,[status(thm)],[f4075,f4009])).
% 0.09/0.55 fof(f4271,plain,(
% 0.09/0.55 $false|~sQ639_spl|~sQ641_spl|~sQ119_spl),
% 0.09/0.55 inference(forward_subsumption_resolution,[status(thm)],[f4222,f91])).
% 0.09/0.55 fof(f4272,plain,(
% 0.09/0.55 ~sQ639_spl|~sQ641_spl|~sQ119_spl),
% 0.09/0.55 inference(contradiction_clause,[status(thm)],[f4271])).
% 0.09/0.55 fof(f4273,plain,(
% 0.09/0.55 $false|sQ640_spl),
% 0.09/0.55 inference(forward_subsumption_resolution,[status(thm)],[f3951,f89])).
% 0.09/0.55 fof(f4274,plain,(
% 0.09/0.55 sQ640_spl),
% 0.09/0.55 inference(contradiction_clause,[status(thm)],[f4273])).
% 0.09/0.55 fof(f4275,plain,(
% 0.09/0.55 $false),
% 0.09/0.55 inference(sat_refutation,[status(thm)],[f120,f130,f194,f196,f213,f215,f242,f287,f623,f679,f681,f683,f688,f693,f960,f995,f3952,f3956,f4272,f4274])).
% 0.09/0.55 % SZS output end CNFRefutation for theBenchmark.p
% 0.26/0.56 % Elapsed time: 0.183945 seconds
% 0.26/0.56 % CPU time: 1.157067 seconds
% 0.26/0.56 % Total memory used: 102.225 MB
% 0.26/0.56 % Net memory used: 100.097 MB
%------------------------------------------------------------------------------