%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO076-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 : n004.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.10s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO076-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.10/0.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 09:52:34 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.50 % Refutation found
% 0.10/0.50 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.50 fof(f1,axiom,(
% 0.10/0.50 (![Z1,Z2]: (( on(Z1,line_from_to(Z1,Z2))| Z1 = Z2| ~ point(Z1)| ~ point(Z2) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f2,axiom,(
% 0.10/0.50 (![Z2,Z1]: (( on(Z2,line_from_to(Z1,Z2))| Z1 = Z2| ~ point(Z1)| ~ point(Z2) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f3,axiom,(
% 0.10/0.50 (![Z1,Z2]: (( line(line_from_to(Z1,Z2))| Z1 = Z2| ~ point(Z1)| ~ point(Z2) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f4,axiom,(
% 0.10/0.50 (![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.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f5,axiom,(
% 0.10/0.50 (![Y1]: (( on(point_1_on_line(Y1),Y1)| ~ line(Y1) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f6,axiom,(
% 0.10/0.50 (![Y1]: (( on(point_2_on_line(Y1),Y1)| ~ line(Y1) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f7,axiom,(
% 0.10/0.50 (![Y1]: (( point(point_1_on_line(Y1))| ~ line(Y1) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f8,axiom,(
% 0.10/0.50 (![Y1]: (( point(point_2_on_line(Y1))| ~ line(Y1) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f9,axiom,(
% 0.10/0.50 (![Y1]: (( point_1_on_line(Y1) != point_2_on_line(Y1)| ~ line(Y1) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f10,axiom,(
% 0.10/0.50 (![Y1]: (( ~ on(point_not_on_line(Y1),Y1)| ~ line(Y1) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f11,axiom,(
% 0.10/0.50 (![Y1]: (( point(point_not_on_line(Y1))| ~ line(Y1) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f12,axiom,(
% 0.10/0.50 line(at_least_one_line) ),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f32,hypothesis,(
% 0.10/0.50 point(a_point) ),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f33,negated_conjecture,(
% 0.10/0.50 (![Line]: (( ~ line(Line)| on(a_point,Line) ) ))),
% 0.10/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50 fof(f34,plain,(
% 0.10/0.50 ![Z2]: ((![Z1]: ((on(Z1,line_from_to(Z1,Z2))|Z1=Z2)|~point(Z1)))|~point(Z2))),
% 0.10/0.50 inference(miniscoping,[status(thm)],[f1])).
% 0.10/0.50 fof(f35,plain,(
% 0.10/0.50 ![X0,X1]: (on(X0,line_from_to(X0,X1))|X0=X1|~point(X0)|~point(X1))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f34])).
% 0.10/0.50 fof(f36,plain,(
% 0.10/0.50 ![Z2]: ((![Z1]: ((on(Z2,line_from_to(Z1,Z2))|Z1=Z2)|~point(Z1)))|~point(Z2))),
% 0.10/0.50 inference(miniscoping,[status(thm)],[f2])).
% 0.10/0.50 fof(f37,plain,(
% 0.10/0.50 ![X0,X1]: (on(X0,line_from_to(X1,X0))|X1=X0|~point(X1)|~point(X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f36])).
% 0.10/0.50 fof(f38,plain,(
% 0.10/0.50 ![Z2]: ((![Z1]: ((line(line_from_to(Z1,Z2))|Z1=Z2)|~point(Z1)))|~point(Z2))),
% 0.10/0.50 inference(miniscoping,[status(thm)],[f3])).
% 0.10/0.50 fof(f39,plain,(
% 0.10/0.50 ![X0,X1]: (line(line_from_to(X0,X1))|X0=X1|~point(X0)|~point(X1))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f38])).
% 0.10/0.50 fof(f40,plain,(
% 0.10/0.50 ![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.10/0.50 inference(miniscoping,[status(thm)],[f4])).
% 0.10/0.50 fof(f41,plain,(
% 0.10/0.50 ![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.10/0.50 inference(cnf_transformation,[status(thm)],[f40])).
% 0.10/0.50 fof(f42,plain,(
% 0.10/0.50 ![X0]: (on(point_1_on_line(X0),X0)|~line(X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.50 fof(f43,plain,(
% 0.10/0.50 ![X0]: (on(point_2_on_line(X0),X0)|~line(X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.50 fof(f44,plain,(
% 0.10/0.50 ![X0]: (point(point_1_on_line(X0))|~line(X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f7])).
% 0.10/0.50 fof(f45,plain,(
% 0.10/0.50 ![X0]: (point(point_2_on_line(X0))|~line(X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.50 fof(f46,plain,(
% 0.10/0.50 ![X0]: (~point_1_on_line(X0)=point_2_on_line(X0)|~line(X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f9])).
% 0.10/0.50 fof(f47,plain,(
% 0.10/0.50 ![X0]: (~on(point_not_on_line(X0),X0)|~line(X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f10])).
% 0.10/0.50 fof(f48,plain,(
% 0.10/0.50 ![X0]: (point(point_not_on_line(X0))|~line(X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f11])).
% 0.10/0.50 fof(f49,plain,(
% 0.10/0.50 line(at_least_one_line)),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f12])).
% 0.10/0.50 fof(f76,plain,(
% 0.10/0.50 point(a_point)),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f32])).
% 0.10/0.50 fof(f77,plain,(
% 0.10/0.50 ![X0]: (~line(X0)|on(a_point,X0))),
% 0.10/0.50 inference(cnf_transformation,[status(thm)],[f33])).
% 0.10/0.50 fof(f79,plain,(
% 0.10/0.50 ![X0,X1,X2]: (~on(X0,X1)|X0=X2|~on(X2,X1)|X1=at_least_one_line|~on(X0,at_least_one_line)|~on(X2,at_least_one_line)|~point(X0)|~point(X2)|~line(X1))),
% 0.10/0.50 inference(resolution,[status(thm)],[f49,f41])).
% 0.10/0.50 fof(f80,plain,(
% 0.10/0.50 ![X0,X1]: (~on(X0,X1)|X0=a_point|~on(a_point,X1)|X1=at_least_one_line|~on(X0,at_least_one_line)|~point(X0)|~point(a_point)|~line(X1)|~line(at_least_one_line))),
% 0.10/0.50 inference(resolution,[status(thm)],[f79,f77])).
% 0.10/0.50 fof(f81,plain,(
% 0.10/0.50 ![X0,X1]: (~on(X0,X1)|X0=a_point|X1=at_least_one_line|~on(X0,at_least_one_line)|~point(X0)|~point(a_point)|~line(X1)|~line(at_least_one_line))),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f80,f77])).
% 0.10/0.50 fof(f82,plain,(
% 0.10/0.50 ![X0,X1]: (~on(X0,X1)|X0=a_point|X1=at_least_one_line|~on(X0,at_least_one_line)|~point(X0)|~line(X1)|~line(at_least_one_line))),
% 0.10/0.50 inference(resolution,[status(thm)],[f81,f76])).
% 0.10/0.50 fof(f83,plain,(
% 0.10/0.50 ![X0,X1]: (~on(X0,X1)|X0=a_point|X1=at_least_one_line|~on(X0,at_least_one_line)|~point(X0)|~line(X1))),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f82,f49])).
% 0.10/0.50 fof(f87,plain,(
% 0.10/0.50 ![X0]: (~line(at_least_one_line)|~on(point_1_on_line(at_least_one_line),X0)|point_1_on_line(at_least_one_line)=a_point|X0=at_least_one_line|~point(point_1_on_line(at_least_one_line))|~line(X0))),
% 0.10/0.50 inference(resolution,[status(thm)],[f42,f83])).
% 0.10/0.50 fof(f89,plain,(
% 0.10/0.50 ![X0]: (~on(point_1_on_line(at_least_one_line),X0)|point_1_on_line(at_least_one_line)=a_point|X0=at_least_one_line|~point(point_1_on_line(at_least_one_line))|~line(X0))),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f87,f49])).
% 0.10/0.50 fof(f91,plain,(
% 0.10/0.50 ![X0]: (~line(at_least_one_line)|~on(point_2_on_line(at_least_one_line),X0)|point_2_on_line(at_least_one_line)=a_point|X0=at_least_one_line|~point(point_2_on_line(at_least_one_line))|~line(X0))),
% 0.10/0.50 inference(resolution,[status(thm)],[f43,f83])).
% 0.10/0.50 fof(f93,plain,(
% 0.10/0.50 ![X0]: (~on(point_2_on_line(at_least_one_line),X0)|point_2_on_line(at_least_one_line)=a_point|X0=at_least_one_line|~point(point_2_on_line(at_least_one_line))|~line(X0))),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f91,f49])).
% 0.10/0.50 fof(f96,plain,(
% 0.10/0.50 ~point_1_on_line(at_least_one_line)=point_2_on_line(at_least_one_line)),
% 0.10/0.50 inference(resolution,[status(thm)],[f46,f49])).
% 0.10/0.50 fof(f97,plain,(
% 0.10/0.50 ![X0]: (~on(point_1_on_line(at_least_one_line),X0)|point_1_on_line(at_least_one_line)=a_point|X0=at_least_one_line|~line(X0)|~line(at_least_one_line))),
% 0.10/0.50 inference(resolution,[status(thm)],[f89,f44])).
% 0.10/0.50 fof(f98,plain,(
% 0.10/0.50 ![X0]: (~on(point_1_on_line(at_least_one_line),X0)|point_1_on_line(at_least_one_line)=a_point|X0=at_least_one_line|~line(X0))),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f97,f49])).
% 0.10/0.50 fof(f99,plain,(
% 0.10/0.50 ![X0,X1]: (~on(point_1_on_line(at_least_one_line),line_from_to(X0,X1))|point_1_on_line(at_least_one_line)=a_point|line_from_to(X0,X1)=at_least_one_line|X0=X1|~point(X0)|~point(X1))),
% 0.10/0.50 inference(resolution,[status(thm)],[f98,f39])).
% 0.10/0.50 fof(f101,plain,(
% 0.10/0.50 ![X0]: (~on(point_2_on_line(at_least_one_line),X0)|point_2_on_line(at_least_one_line)=a_point|X0=at_least_one_line|~line(X0)|~line(at_least_one_line))),
% 0.10/0.50 inference(resolution,[status(thm)],[f93,f45])).
% 0.10/0.50 fof(f102,plain,(
% 0.10/0.50 ![X0]: (~on(point_2_on_line(at_least_one_line),X0)|point_2_on_line(at_least_one_line)=a_point|X0=at_least_one_line|~line(X0))),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f101,f49])).
% 0.10/0.50 fof(f103,plain,(
% 0.10/0.50 ![X0,X1]: (~on(point_2_on_line(at_least_one_line),line_from_to(X0,X1))|point_2_on_line(at_least_one_line)=a_point|line_from_to(X0,X1)=at_least_one_line|X0=X1|~point(X0)|~point(X1))),
% 0.10/0.50 inference(resolution,[status(thm)],[f102,f39])).
% 0.10/0.50 fof(f105,plain,(
% 0.10/0.50 ![X0]: (point_1_on_line(at_least_one_line)=a_point|line_from_to(X0,point_1_on_line(at_least_one_line))=at_least_one_line|X0=point_1_on_line(at_least_one_line)|~point(X0)|~point(point_1_on_line(at_least_one_line))|X0=point_1_on_line(at_least_one_line)|~point(X0)|~point(point_1_on_line(at_least_one_line)))),
% 0.10/0.50 inference(resolution,[status(thm)],[f99,f37])).
% 0.10/0.50 fof(f107,plain,(
% 0.10/0.50 ![X0]: (point_1_on_line(at_least_one_line)=a_point|line_from_to(X0,point_1_on_line(at_least_one_line))=at_least_one_line|X0=point_1_on_line(at_least_one_line)|~point(X0)|~point(point_1_on_line(at_least_one_line)))),
% 0.10/0.50 inference(duplicate_literals_removal,[status(thm)],[f105])).
% 0.10/0.50 fof(f109,plain,(
% 0.10/0.50 ![X0]: (point_2_on_line(at_least_one_line)=a_point|line_from_to(X0,point_2_on_line(at_least_one_line))=at_least_one_line|X0=point_2_on_line(at_least_one_line)|~point(X0)|~point(point_2_on_line(at_least_one_line))|X0=point_2_on_line(at_least_one_line)|~point(X0)|~point(point_2_on_line(at_least_one_line)))),
% 0.10/0.50 inference(resolution,[status(thm)],[f103,f37])).
% 0.10/0.50 fof(f111,plain,(
% 0.10/0.50 ![X0]: (point_2_on_line(at_least_one_line)=a_point|line_from_to(X0,point_2_on_line(at_least_one_line))=at_least_one_line|X0=point_2_on_line(at_least_one_line)|~point(X0)|~point(point_2_on_line(at_least_one_line)))),
% 0.10/0.50 inference(duplicate_literals_removal,[status(thm)],[f109])).
% 0.10/0.50 fof(f113,plain,(
% 0.10/0.50 ![X0]: (point_1_on_line(at_least_one_line)=a_point|line_from_to(X0,point_1_on_line(at_least_one_line))=at_least_one_line|X0=point_1_on_line(at_least_one_line)|~point(X0)|~line(at_least_one_line))),
% 0.10/0.50 inference(resolution,[status(thm)],[f107,f44])).
% 0.10/0.50 fof(f114,plain,(
% 0.10/0.50 ![X0]: (point_1_on_line(at_least_one_line)=a_point|line_from_to(X0,point_1_on_line(at_least_one_line))=at_least_one_line|X0=point_1_on_line(at_least_one_line)|~point(X0))),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f113,f49])).
% 0.10/0.50 fof(f117,plain,(
% 0.10/0.50 ![X0]: (point_1_on_line(at_least_one_line)=a_point|line_from_to(point_not_on_line(X0),point_1_on_line(at_least_one_line))=at_least_one_line|point_not_on_line(X0)=point_1_on_line(at_least_one_line)|~line(X0))),
% 0.10/0.50 inference(resolution,[status(thm)],[f114,f48])).
% 0.10/0.50 fof(f155,plain,(
% 0.10/0.50 point_1_on_line(at_least_one_line)=a_point|line_from_to(point_not_on_line(at_least_one_line),point_1_on_line(at_least_one_line))=at_least_one_line|point_not_on_line(at_least_one_line)=point_1_on_line(at_least_one_line)),
% 0.10/0.50 inference(resolution,[status(thm)],[f117,f49])).
% 0.10/0.50 fof(f161,plain,(
% 0.10/0.50 on(point_not_on_line(at_least_one_line),at_least_one_line)|point_not_on_line(at_least_one_line)=point_1_on_line(at_least_one_line)|~point(point_not_on_line(at_least_one_line))|~point(point_1_on_line(at_least_one_line))|point_1_on_line(at_least_one_line)=a_point|point_not_on_line(at_least_one_line)=point_1_on_line(at_least_one_line)),
% 0.10/0.50 inference(paramodulation,[status(thm)],[f155,f35])).
% 0.10/0.50 fof(f167,plain,(
% 0.10/0.50 on(point_not_on_line(at_least_one_line),at_least_one_line)|point_not_on_line(at_least_one_line)=point_1_on_line(at_least_one_line)|~point(point_not_on_line(at_least_one_line))|~point(point_1_on_line(at_least_one_line))|point_1_on_line(at_least_one_line)=a_point),
% 0.10/0.50 inference(duplicate_literals_removal,[status(thm)],[f161])).
% 0.10/0.50 fof(f208,plain,(
% 0.10/0.50 ![X0]: (point_2_on_line(at_least_one_line)=a_point|line_from_to(X0,point_2_on_line(at_least_one_line))=at_least_one_line|X0=point_2_on_line(at_least_one_line)|~point(X0)|~line(at_least_one_line))),
% 0.10/0.50 inference(resolution,[status(thm)],[f111,f45])).
% 0.10/0.50 fof(f209,plain,(
% 0.10/0.50 ![X0]: (point_2_on_line(at_least_one_line)=a_point|line_from_to(X0,point_2_on_line(at_least_one_line))=at_least_one_line|X0=point_2_on_line(at_least_one_line)|~point(X0))),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f208,f49])).
% 0.10/0.50 fof(f214,plain,(
% 0.10/0.50 ![X0]: (point_2_on_line(at_least_one_line)=a_point|line_from_to(point_not_on_line(X0),point_2_on_line(at_least_one_line))=at_least_one_line|point_not_on_line(X0)=point_2_on_line(at_least_one_line)|~line(X0))),
% 0.10/0.50 inference(resolution,[status(thm)],[f209,f48])).
% 0.10/0.50 fof(f276,plain,(
% 0.10/0.50 point_2_on_line(at_least_one_line)=a_point|line_from_to(point_not_on_line(at_least_one_line),point_2_on_line(at_least_one_line))=at_least_one_line|point_not_on_line(at_least_one_line)=point_2_on_line(at_least_one_line)),
% 0.10/0.50 inference(resolution,[status(thm)],[f214,f49])).
% 0.10/0.50 fof(f282,plain,(
% 0.10/0.50 on(point_not_on_line(at_least_one_line),at_least_one_line)|point_not_on_line(at_least_one_line)=point_2_on_line(at_least_one_line)|~point(point_not_on_line(at_least_one_line))|~point(point_2_on_line(at_least_one_line))|point_2_on_line(at_least_one_line)=a_point|point_not_on_line(at_least_one_line)=point_2_on_line(at_least_one_line)),
% 0.10/0.50 inference(paramodulation,[status(thm)],[f276,f35])).
% 0.10/0.50 fof(f288,plain,(
% 0.10/0.50 on(point_not_on_line(at_least_one_line),at_least_one_line)|point_not_on_line(at_least_one_line)=point_2_on_line(at_least_one_line)|~point(point_not_on_line(at_least_one_line))|~point(point_2_on_line(at_least_one_line))|point_2_on_line(at_least_one_line)=a_point),
% 0.10/0.50 inference(duplicate_literals_removal,[status(thm)],[f282])).
% 0.10/0.50 fof(f430,plain,(
% 0.10/0.50 on(point_not_on_line(at_least_one_line),at_least_one_line)|point_not_on_line(at_least_one_line)=point_1_on_line(at_least_one_line)|~point(point_not_on_line(at_least_one_line))|point_1_on_line(at_least_one_line)=a_point|~line(at_least_one_line)),
% 0.10/0.50 inference(resolution,[status(thm)],[f167,f44])).
% 0.10/0.50 fof(f431,plain,(
% 0.10/0.50 point_not_on_line(at_least_one_line)=point_1_on_line(at_least_one_line)|~point(point_not_on_line(at_least_one_line))|point_1_on_line(at_least_one_line)=a_point|~line(at_least_one_line)),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f430,f47])).
% 0.10/0.50 fof(f432,plain,(
% 0.10/0.50 point_not_on_line(at_least_one_line)=point_1_on_line(at_least_one_line)|point_1_on_line(at_least_one_line)=a_point|~line(at_least_one_line)|~line(at_least_one_line)),
% 0.10/0.50 inference(resolution,[status(thm)],[f431,f48])).
% 0.10/0.50 fof(f433,plain,(
% 0.10/0.50 point_not_on_line(at_least_one_line)=point_1_on_line(at_least_one_line)|point_1_on_line(at_least_one_line)=a_point|~line(at_least_one_line)),
% 0.10/0.50 inference(duplicate_literals_removal,[status(thm)],[f432])).
% 0.10/0.50 fof(f434,plain,(
% 0.10/0.50 point_not_on_line(at_least_one_line)=point_1_on_line(at_least_one_line)|point_1_on_line(at_least_one_line)=a_point),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f433,f49])).
% 0.10/0.50 fof(f449,plain,(
% 0.10/0.50 on(point_not_on_line(at_least_one_line),at_least_one_line)|~line(at_least_one_line)|point_1_on_line(at_least_one_line)=a_point),
% 0.10/0.50 inference(paramodulation,[status(thm)],[f434,f42])).
% 0.10/0.50 fof(f462,plain,(
% 0.10/0.50 ~line(at_least_one_line)|point_1_on_line(at_least_one_line)=a_point),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f449,f47])).
% 0.10/0.50 fof(f463,plain,(
% 0.10/0.50 point_1_on_line(at_least_one_line)=a_point),
% 0.10/0.50 inference(resolution,[status(thm)],[f462,f49])).
% 0.10/0.50 fof(f495,plain,(
% 0.10/0.50 ~a_point=point_2_on_line(at_least_one_line)),
% 0.10/0.50 inference(backward_demodulation,[status(thm)],[f463,f96])).
% 0.10/0.50 fof(f557,plain,(
% 0.10/0.50 on(point_not_on_line(at_least_one_line),at_least_one_line)|point_not_on_line(at_least_one_line)=point_2_on_line(at_least_one_line)|~point(point_not_on_line(at_least_one_line))|~point(point_2_on_line(at_least_one_line))),
% 0.10/0.50 inference(backward_subsumption_resolution,[status(thm)],[f288,f495])).
% 0.10/0.50 fof(f660,plain,(
% 0.10/0.50 on(point_not_on_line(at_least_one_line),at_least_one_line)|point_not_on_line(at_least_one_line)=point_2_on_line(at_least_one_line)|~point(point_not_on_line(at_least_one_line))|~line(at_least_one_line)),
% 0.10/0.50 inference(resolution,[status(thm)],[f557,f45])).
% 0.10/0.50 fof(f661,plain,(
% 0.10/0.50 point_not_on_line(at_least_one_line)=point_2_on_line(at_least_one_line)|~point(point_not_on_line(at_least_one_line))|~line(at_least_one_line)),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f660,f47])).
% 0.10/0.50 fof(f662,plain,(
% 0.10/0.50 point_not_on_line(at_least_one_line)=point_2_on_line(at_least_one_line)|~line(at_least_one_line)|~line(at_least_one_line)),
% 0.10/0.50 inference(resolution,[status(thm)],[f661,f48])).
% 0.10/0.50 fof(f663,plain,(
% 0.10/0.50 point_not_on_line(at_least_one_line)=point_2_on_line(at_least_one_line)|~line(at_least_one_line)),
% 0.10/0.50 inference(duplicate_literals_removal,[status(thm)],[f662])).
% 0.10/0.50 fof(f701,plain,(
% 0.10/0.50 point_not_on_line(at_least_one_line)=point_2_on_line(at_least_one_line)),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f663,f49])).
% 0.10/0.51 fof(f727,plain,(
% 0.10/0.51 on(point_not_on_line(at_least_one_line),at_least_one_line)|~line(at_least_one_line)),
% 0.10/0.51 inference(paramodulation,[status(thm)],[f701,f43])).
% 0.10/0.51 fof(f730,plain,(
% 0.10/0.51 ~line(at_least_one_line)),
% 0.10/0.51 inference(forward_subsumption_resolution,[status(thm)],[f727,f47])).
% 0.10/0.51 fof(f731,plain,(
% 0.10/0.51 $false),
% 0.10/0.51 inference(backward_subsumption_resolution,[status(thm)],[f49,f730])).
% 0.10/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.53 % Elapsed time: 0.148250 seconds
% 0.10/0.53 % CPU time: 0.919971 seconds
% 0.10/0.53 % Total memory used: 93.464 MB
% 0.10/0.53 % Net memory used: 92.091 MB
%------------------------------------------------------------------------------