%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO077-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -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:23:59 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.64s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 30
% Syntax : Number of formulae : 91 ( 30 unt; 14 def)
% Number of atoms : 305 ( 67 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 366 ( 152 ~; 200 |; 0 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 15 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-3 aty)
% Number of variables : 45 ( 45 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [Z1,Y3,Z2,Y4] :
( ~ line(Y4)
| ~ line(Y3)
| ~ point(Z2)
| ~ point(Z1)
| ~ on(Z2,Y4)
| ~ on(Z1,Y4)
| Y3 = Y4
| ~ on(Z2,Y3)
| Z1 = Z2
| ~ on(Z1,Y3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [X1,X2,X3] :
( ~ collinear(X1,X2,X3)
| on(X1,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [X1,X2,X3] :
( ~ collinear(X1,X2,X3)
| on(X2,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
! [X1,X2,X3] :
( ~ collinear(X1,X2,X3)
| on(X3,line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X1,X2,X3] :
( ~ collinear(X1,X2,X3)
| line(line_through_3_points(X1,X2,X3))
| X2 = X3
| X1 = X3
| X1 = X2
| ~ point(X3)
| ~ point(X2)
| ~ point(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,hypothesis,
point(point1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,hypothesis,
point(point2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,hypothesis,
point(point3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,hypothesis,
line(a_line),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,hypothesis,
on(point1,a_line),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,hypothesis,
on(point2,a_line),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,hypothesis,
~ on(point3,a_line),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,hypothesis,
point1 != point2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
point1 != point3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,hypothesis,
point2 != point3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
collinear(point1,point2,point3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,plain,
! [Y4] :
( ~ line(Y4)
| ! [Y3] :
( ~ line(Y3)
| ! [Z2] :
( ~ point(Z2)
| ! [Z1] :
( ~ point(Z1)
| ~ on(Z2,Y4)
| ~ on(Z1,Y4)
| Y3 = Y4
| ~ on(Z2,Y3)
| Z1 = Z2
| ~ on(Z1,Y3) ) ) ) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f50,plain,
! [X0,X1,X2,X3] :
( ~ line(X3)
| ~ line(X1)
| ~ point(X2)
| ~ point(X0)
| ~ on(X2,X3)
| ~ on(X0,X3)
| X1 = X3
| ~ on(X2,X1)
| X0 = X2
| ~ on(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f79,plain,
! [X0,X1,X2] :
( ~ collinear(X0,X1,X2)
| on(X0,line_through_3_points(X0,X1,X2))
| X1 = X2
| X0 = X2
| X0 = X1
| ~ point(X2)
| ~ point(X1)
| ~ point(X0) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ~ collinear(X0,X1,X2)
| on(X1,line_through_3_points(X0,X1,X2))
| X1 = X2
| X0 = X2
| X0 = X1
| ~ point(X2)
| ~ point(X1)
| ~ point(X0) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f81,plain,
! [X0,X1,X2] :
( ~ collinear(X0,X1,X2)
| on(X2,line_through_3_points(X0,X1,X2))
| X1 = X2
| X0 = X2
| X0 = X1
| ~ point(X2)
| ~ point(X1)
| ~ point(X0) ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ collinear(X0,X1,X2)
| line(line_through_3_points(X0,X1,X2))
| X1 = X2
| X0 = X2
| X0 = X1
| ~ point(X2)
| ~ point(X1)
| ~ point(X0) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f85,plain,
point(point1),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f86,plain,
point(point2),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f87,plain,
point(point3),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f88,plain,
line(a_line),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f89,plain,
on(point1,a_line),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f90,plain,
on(point2,a_line),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f91,plain,
~ on(point3,a_line),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f92,plain,
point1 != point2,
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f93,plain,
point1 != point3,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f94,plain,
point2 != point3,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f95,plain,
collinear(point1,point2,point3),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f115,definition,
( sQ1_spl
<=> point(point1) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f117,plain,
( sQ1_spl
| ~ point(point1) ),
inference(component_clause,[status(thm)],[f115]) ).
fof(f121,definition,
( sQ3_spl
<=> line(a_line) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f123,plain,
( sQ3_spl
| ~ line(a_line) ),
inference(component_clause,[status(thm)],[f121]) ).
fof(f165,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f117,f85]) ).
fof(f166,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f165]) ).
fof(f167,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f123,f88]) ).
fof(f168,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f167]) ).
fof(f216,definition,
( sQ18_spl
<=> point2 = point3 ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f217,plain,
( ~ sQ18_spl
| point2 = point3 ),
inference(component_clause,[status(thm)],[f216]) ).
fof(f223,definition,
( sQ20_spl
<=> point1 = point3 ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f224,plain,
( ~ sQ20_spl
| point1 = point3 ),
inference(component_clause,[status(thm)],[f223]) ).
fof(f244,plain,
( ~ sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f224,f93]) ).
fof(f245,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f244]) ).
fof(f246,plain,
( ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f217,f94]) ).
fof(f247,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f246]) ).
fof(f265,definition,
( sQ28_spl
<=> point1 = point2 ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f266,plain,
( ~ sQ28_spl
| point1 = point2 ),
inference(component_clause,[status(thm)],[f265]) ).
fof(f284,plain,
( ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f266,f92]) ).
fof(f285,plain,
~ sQ28_spl,
inference(contradiction_clause,[status(thm)],[f284]) ).
fof(f301,plain,
! [X0,X1] :
( ~ line(a_line)
| ~ line(X1)
| ~ point(point2)
| ~ point(X0)
| ~ on(X0,a_line)
| X1 = a_line
| ~ on(point2,X1)
| X0 = point2
| ~ on(X0,X1) ),
inference(resolution,[status(thm)],[f90,f50]) ).
fof(f323,definition,
( sQ35_spl
<=> point(point2) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f325,plain,
( sQ35_spl
| ~ point(point2) ),
inference(component_clause,[status(thm)],[f323]) ).
fof(f335,definition,
! [X0,X1] :
( sQ38_spl
<=> ( ~ line(X1)
| ~ point(X0)
| ~ on(X0,a_line)
| X1 = a_line
| ~ on(point2,X1)
| X0 = point2
| ~ on(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f336,plain,
! [X0,X1] :
( ~ sQ38_spl
| ~ line(X1)
| ~ point(X0)
| ~ on(X0,a_line)
| X1 = a_line
| ~ on(point2,X1)
| X0 = point2
| ~ on(X0,X1) ),
inference(component_clause,[status(thm)],[f335]) ).
fof(f338,plain,
( ~ sQ3_spl
| ~ sQ35_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f301,f335,f323,f121]) ).
fof(f378,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f325,f86]) ).
fof(f379,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f378]) ).
fof(f556,plain,
! [X0] :
( ~ sQ38_spl
| ~ line(X0)
| ~ point(point1)
| X0 = a_line
| ~ on(point2,X0)
| point1 = point2
| ~ on(point1,X0) ),
inference(resolution,[status(thm)],[f336,f89]) ).
fof(f567,definition,
! [X0] :
( sQ73_spl
<=> ( ~ line(X0)
| X0 = a_line
| ~ on(point2,X0)
| ~ on(point1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f568,plain,
! [X0] :
( ~ sQ73_spl
| ~ line(X0)
| X0 = a_line
| ~ on(point2,X0)
| ~ on(point1,X0) ),
inference(component_clause,[status(thm)],[f567]) ).
fof(f570,plain,
( ~ sQ38_spl
| ~ sQ1_spl
| sQ28_spl
| sQ73_spl ),
inference(split_clause,[status(thm)],[f556,f567,f265,f115,f335]) ).
fof(f701,definition,
( sQ92_spl
<=> point(point3) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f703,plain,
( sQ92_spl
| ~ point(point3) ),
inference(component_clause,[status(thm)],[f701]) ).
fof(f755,plain,
( sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f703,f87]) ).
fof(f756,plain,
sQ92_spl,
inference(contradiction_clause,[status(thm)],[f755]) ).
fof(f929,plain,
( on(point1,line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(resolution,[status(thm)],[f79,f95]) ).
fof(f930,definition,
( sQ135_spl
<=> on(point1,line_through_3_points(point1,point2,point3)) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f931,plain,
( ~ sQ135_spl
| on(point1,line_through_3_points(point1,point2,point3)) ),
inference(component_clause,[status(thm)],[f930]) ).
fof(f933,plain,
( sQ135_spl
| sQ18_spl
| sQ20_spl
| sQ28_spl
| ~ sQ92_spl
| ~ sQ35_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f929,f115,f323,f701,f265,f223,f216,f930]) ).
fof(f934,plain,
( on(point2,line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(resolution,[status(thm)],[f80,f95]) ).
fof(f935,definition,
( sQ136_spl
<=> on(point2,line_through_3_points(point1,point2,point3)) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f938,plain,
( sQ136_spl
| sQ18_spl
| sQ20_spl
| sQ28_spl
| ~ sQ92_spl
| ~ sQ35_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f934,f115,f323,f701,f265,f223,f216,f935]) ).
fof(f939,plain,
( on(point3,line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(resolution,[status(thm)],[f81,f95]) ).
fof(f940,definition,
( sQ137_spl
<=> on(point3,line_through_3_points(point1,point2,point3)) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f941,plain,
( ~ sQ137_spl
| on(point3,line_through_3_points(point1,point2,point3)) ),
inference(component_clause,[status(thm)],[f940]) ).
fof(f943,plain,
( sQ137_spl
| sQ18_spl
| sQ20_spl
| sQ28_spl
| ~ sQ92_spl
| ~ sQ35_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f939,f115,f323,f701,f265,f223,f216,f940]) ).
fof(f944,plain,
( line(line_through_3_points(point1,point2,point3))
| point2 = point3
| point1 = point3
| point1 = point2
| ~ point(point3)
| ~ point(point2)
| ~ point(point1) ),
inference(resolution,[status(thm)],[f82,f95]) ).
fof(f945,definition,
( sQ138_spl
<=> line(line_through_3_points(point1,point2,point3)) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f948,plain,
( sQ138_spl
| sQ18_spl
| sQ20_spl
| sQ28_spl
| ~ sQ92_spl
| ~ sQ35_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f944,f115,f323,f701,f265,f223,f216,f945]) ).
fof(f949,plain,
( ~ sQ73_spl
| ~ sQ135_spl
| ~ line(line_through_3_points(point1,point2,point3))
| line_through_3_points(point1,point2,point3) = a_line
| ~ on(point2,line_through_3_points(point1,point2,point3)) ),
inference(resolution,[status(thm)],[f931,f568]) ).
fof(f980,definition,
( sQ139_spl
<=> line_through_3_points(point1,point2,point3) = a_line ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f981,plain,
( ~ sQ139_spl
| line_through_3_points(point1,point2,point3) = a_line ),
inference(component_clause,[status(thm)],[f980]) ).
fof(f983,plain,
( ~ sQ73_spl
| ~ sQ135_spl
| ~ sQ138_spl
| sQ139_spl
| ~ sQ136_spl ),
inference(split_clause,[status(thm)],[f949,f935,f980,f945,f930,f567]) ).
fof(f1065,plain,
( ~ sQ137_spl
| ~ sQ139_spl
| on(point3,a_line) ),
inference(backward_demodulation,[status(thm)],[f981,f941]) ).
fof(f1075,plain,
( ~ sQ137_spl
| ~ sQ139_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1065,f91]) ).
fof(f1076,plain,
( ~ sQ137_spl
| ~ sQ139_spl ),
inference(contradiction_clause,[status(thm)],[f1075]) ).
fof(f1077,plain,
$false,
inference(sat_refutation,[status(thm)],[f166,f168,f245,f247,f285,f338,f379,f570,f756,f933,f938,f943,f948,f983,f1076]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO077-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n001.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 20 09:58:58 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.64 % Refutation found
% 0.09/0.64 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.58/0.67 % Elapsed time: 0.285074 seconds
% 1.58/0.67 % CPU time: 1.895298 seconds
% 1.58/0.67 % Total memory used: 101.368 MB
% 1.58/0.67 % Net memory used: 99.666 MB
%------------------------------------------------------------------------------