%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO284+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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:24:49 PM UTC 2026
% Result : Theorem 0.15s 10.66s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 5
% Syntax : Number of formulae : 70 ( 22 unt; 0 def)
% Number of atoms : 309 ( 79 equ)
% Maximal formula atoms : 11 ( 4 avg)
% Number of connectives : 448 ( 209 ~; 197 |; 40 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 105 ( 93 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
? [Vd1151,Vd1152] :
( rline(Vd1151)
& ron(vd1123,Vd1151)
& ron(vd1125,Vd1151)
& rcircle(Vd1152)
& rcenter(vd1123,Vd1152)
& ron(vd1127,Vd1152) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ? [Vd1151,Vd1152] :
( rline(Vd1151)
& ron(vd1123,Vd1151)
& ron(vd1125,Vd1151)
& rcircle(Vd1152)
& rcenter(vd1123,Vd1152)
& ron(vd1127,Vd1152) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
vd1123 = vd1129,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
( rpoint(vd1124)
& vd1123 = vd1124
& rpoint(vd1126)
& vd1125 = vd1126
& rpoint(vd1128)
& vd1127 = vd1128
& rpoint(vd1130)
& vd1129 = vd1130
& vd1123 != vd1125
& vd1127 != vd1129
& rless(vf(vd1127,vd1129),vf(vd1123,vd1125)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [Vd225,Vd226] :
( ( ? [Vd229] :
( rpoint(Vd229)
& Vd225 = Vd229 )
& ? [Vd230] :
( rpoint(Vd230)
& Vd226 = Vd230 )
& Vd225 != Vd226 )
=> ? [Vd231] :
( rcircle(Vd231)
& rcenter(Vd225,Vd231)
& ron(Vd226,Vd231) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [Vd217,Vd218] :
( ( ? [Vd220] :
( rpoint(Vd220)
& Vd217 = Vd220 )
& ? [Vd221] :
( rpoint(Vd221)
& Vd218 = Vd221 )
& Vd217 != Vd218 )
=> ? [Vd223] :
( rline(Vd223)
& ron(Vd217,Vd223)
& ron(Vd218,Vd223) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f133,plain,
! [Vd1151,Vd1152] :
( ~ rline(Vd1151)
| ~ ron(vd1123,Vd1151)
| ~ ron(vd1125,Vd1151)
| ~ rcircle(Vd1152)
| ~ rcenter(vd1123,Vd1152)
| ~ ron(vd1127,Vd1152) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f134,plain,
! [Vd1151] :
( ~ rline(Vd1151)
| ~ ron(vd1123,Vd1151)
| ~ ron(vd1125,Vd1151)
| ! [Vd1152] :
( ~ rcircle(Vd1152)
| ~ rcenter(vd1123,Vd1152)
| ~ ron(vd1127,Vd1152) ) ),
inference(miniscoping,[status(thm)],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ ron(vd1123,X1)
| ~ ron(vd1125,X1)
| ~ rcircle(X0)
| ~ rcenter(vd1123,X0)
| ~ ron(vd1127,X0) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f136,plain,
vd1123 = vd1129,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f160,plain,
vd1127 != vd1129,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f161,plain,
vd1123 != vd1125,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f162,plain,
vd1129 = vd1130,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f164,plain,
vd1127 = vd1128,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f165,plain,
rpoint(vd1128),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f166,plain,
vd1125 = vd1126,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f167,plain,
rpoint(vd1126),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f168,plain,
vd1123 = vd1124,
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f169,plain,
rpoint(vd1124),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f199,plain,
! [Vd225,Vd226] :
( ? [Vd231] :
( rcircle(Vd231)
& rcenter(Vd225,Vd231)
& ron(Vd226,Vd231) )
| ! [Vd229] :
( ~ rpoint(Vd229)
| Vd225 != Vd229 )
| ! [Vd230] :
( ~ rpoint(Vd230)
| Vd226 != Vd230 )
| Vd225 = Vd226 ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f200,plain,
! [Vd225,Vd226] :
( ( rcircle(sK2_skl(Vd226,Vd225))
& rcenter(Vd225,sK2_skl(Vd226,Vd225))
& ron(Vd226,sK2_skl(Vd226,Vd225)) )
| ! [Vd229] :
( ~ rpoint(Vd229)
| Vd225 != Vd229 )
| ! [Vd230] :
( ~ rpoint(Vd230)
| Vd226 != Vd230 )
| Vd225 = Vd226 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Vd231,sK2_skl(Vd226,Vd225))],[f199]) ).
fof(f201,plain,
! [X0,X1,X2,X3] :
( ron(X1,sK2_skl(X1,X0))
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
! [X0,X1,X2,X3] :
( rcenter(X0,sK2_skl(X1,X0))
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f203,plain,
! [X0,X1,X2,X3] :
( rcircle(sK2_skl(X1,X0))
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f239,plain,
! [Vd217,Vd218] :
( ? [Vd223] :
( rline(Vd223)
& ron(Vd217,Vd223)
& ron(Vd218,Vd223) )
| ! [Vd220] :
( ~ rpoint(Vd220)
| Vd217 != Vd220 )
| ! [Vd221] :
( ~ rpoint(Vd221)
| Vd218 != Vd221 )
| Vd217 = Vd218 ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f240,plain,
! [Vd217,Vd218] :
( ( rline(sK4_skl(Vd218,Vd217))
& ron(Vd217,sK4_skl(Vd218,Vd217))
& ron(Vd218,sK4_skl(Vd218,Vd217)) )
| ! [Vd220] :
( ~ rpoint(Vd220)
| Vd217 != Vd220 )
| ! [Vd221] :
( ~ rpoint(Vd221)
| Vd218 != Vd221 )
| Vd217 = Vd218 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(Vd223,sK4_skl(Vd218,Vd217))],[f239]) ).
fof(f241,plain,
! [X0,X1,X2,X3] :
( ron(X1,sK4_skl(X1,X0))
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f242,plain,
! [X0,X1,X2,X3] :
( ron(X0,sK4_skl(X1,X0))
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f243,plain,
! [X0,X1,X2,X3] :
( rline(sK4_skl(X1,X0))
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f708,plain,
! [X0,X1] :
( ron(X1,sK2_skl(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f201]) ).
fof(f709,plain,
! [X0,X1] :
( rcenter(X0,sK2_skl(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f202]) ).
fof(f710,plain,
! [X0,X1] :
( rcircle(sK2_skl(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f203]) ).
fof(f715,plain,
! [X0,X1] :
( ron(X1,sK4_skl(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f241]) ).
fof(f716,plain,
! [X0,X1] :
( ron(X0,sK4_skl(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f242]) ).
fof(f717,plain,
! [X0,X1] :
( rline(sK4_skl(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f243]) ).
fof(f929,plain,
vd1129 != vd1125,
inference(backward_demodulation,[status(thm)],[f136,f161]) ).
fof(f930,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ ron(vd1129,X1)
| ~ ron(vd1125,X1)
| ~ rcircle(X0)
| ~ rcenter(vd1123,X0)
| ~ ron(vd1127,X0) ),
inference(backward_demodulation,[status(thm)],[f136,f135]) ).
fof(f931,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ ron(vd1129,X1)
| ~ ron(vd1125,X1)
| ~ rcircle(X0)
| ~ rcenter(vd1129,X0)
| ~ ron(vd1127,X0) ),
inference(forward_demodulation,[status(thm)],[f136,f930]) ).
fof(f932,plain,
vd1127 != vd1130,
inference(backward_demodulation,[status(thm)],[f162,f160]) ).
fof(f933,plain,
vd1123 = vd1130,
inference(backward_demodulation,[status(thm)],[f162,f136]) ).
fof(f945,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ ron(vd1129,X1)
| ~ ron(vd1125,X1)
| ~ rcircle(X0)
| ~ rcenter(vd1129,X0)
| ~ ron(vd1128,X0) ),
inference(forward_demodulation,[status(thm)],[f164,f931]) ).
fof(f946,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ ron(vd1129,X1)
| ~ ron(vd1125,X1)
| ~ rcircle(X0)
| ~ rcenter(vd1130,X0)
| ~ ron(vd1128,X0) ),
inference(forward_demodulation,[status(thm)],[f162,f945]) ).
fof(f947,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ ron(vd1129,X1)
| ~ ron(vd1126,X1)
| ~ rcircle(X0)
| ~ rcenter(vd1130,X0)
| ~ ron(vd1128,X0) ),
inference(forward_demodulation,[status(thm)],[f166,f946]) ).
fof(f948,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ ron(vd1130,X1)
| ~ ron(vd1126,X1)
| ~ rcircle(X0)
| ~ rcenter(vd1130,X0)
| ~ ron(vd1128,X0) ),
inference(forward_demodulation,[status(thm)],[f162,f947]) ).
fof(f949,plain,
vd1130 != vd1125,
inference(forward_demodulation,[status(thm)],[f162,f929]) ).
fof(f950,plain,
vd1130 != vd1126,
inference(forward_demodulation,[status(thm)],[f166,f949]) ).
fof(f957,plain,
vd1128 != vd1130,
inference(forward_demodulation,[status(thm)],[f164,f932]) ).
fof(f958,plain,
vd1128 != vd1124,
inference(backward_demodulation,[status(thm)],[f965,f957]) ).
fof(f960,plain,
vd1124 != vd1126,
inference(backward_demodulation,[status(thm)],[f965,f950]) ).
fof(f961,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ ron(vd1124,X1)
| ~ ron(vd1126,X1)
| ~ rcircle(X0)
| ~ rcenter(vd1130,X0)
| ~ ron(vd1128,X0) ),
inference(backward_demodulation,[status(thm)],[f965,f948]) ).
fof(f965,plain,
vd1124 = vd1130,
inference(forward_demodulation,[status(thm)],[f168,f933]) ).
fof(f967,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ ron(vd1124,X1)
| ~ ron(vd1126,X1)
| ~ rcircle(X0)
| ~ rcenter(vd1124,X0)
| ~ ron(vd1128,X0) ),
inference(forward_demodulation,[status(thm)],[f965,f961]) ).
fof(f1367,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ ron(vd1124,X1)
| ~ ron(vd1126,X1)
| ~ rcircle(sK2_skl(vd1128,X0))
| ~ rcenter(vd1124,sK2_skl(vd1128,X0))
| ~ rpoint(X0)
| ~ rpoint(vd1128)
| X0 = vd1128 ),
inference(resolution,[status(thm)],[f708,f967]) ).
fof(f1405,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ ron(vd1124,X1)
| ~ ron(vd1126,X1)
| ~ rcircle(sK2_skl(vd1128,X0))
| ~ rcenter(vd1124,sK2_skl(vd1128,X0))
| ~ rpoint(X0)
| X0 = vd1128 ),
inference(forward_subsumption_resolution,[status(thm)],[f1367,f165]) ).
fof(f1615,plain,
! [X0] :
( ~ rpoint(vd1124)
| ~ rpoint(vd1128)
| vd1124 = vd1128
| ~ rline(X0)
| ~ ron(vd1124,X0)
| ~ ron(vd1126,X0)
| ~ rcircle(sK2_skl(vd1128,vd1124))
| ~ rpoint(vd1124)
| vd1124 = vd1128 ),
inference(resolution,[status(thm)],[f1405,f709]) ).
fof(f1616,plain,
! [X0] :
( ~ rpoint(vd1128)
| ~ rline(X0)
| ~ ron(vd1124,X0)
| ~ ron(vd1126,X0)
| ~ rcircle(sK2_skl(vd1128,vd1124))
| ~ rpoint(vd1124)
| vd1124 = vd1128 ),
inference(duplicate_literals_removal,[status(thm)],[f1615]) ).
fof(f1617,plain,
! [X0] :
( ~ rpoint(vd1128)
| ~ rline(X0)
| ~ ron(vd1124,X0)
| ~ ron(vd1126,X0)
| ~ rcircle(sK2_skl(vd1128,vd1124))
| ~ rpoint(vd1124) ),
inference(forward_subsumption_resolution,[status(thm)],[f1616,f958]) ).
fof(f1618,plain,
! [X0] :
( ~ rpoint(vd1128)
| ~ rline(X0)
| ~ ron(vd1124,X0)
| ~ ron(vd1126,X0)
| ~ rcircle(sK2_skl(vd1128,vd1124)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1617,f169]) ).
fof(f1619,plain,
! [X0] :
( ~ rpoint(vd1124)
| ~ rpoint(vd1128)
| vd1124 = vd1128
| ~ rpoint(vd1128)
| ~ rline(X0)
| ~ ron(vd1124,X0)
| ~ ron(vd1126,X0) ),
inference(resolution,[status(thm)],[f1618,f710]) ).
fof(f1620,plain,
! [X0] :
( ~ rpoint(vd1124)
| vd1124 = vd1128
| ~ rpoint(vd1128)
| ~ rline(X0)
| ~ ron(vd1124,X0)
| ~ ron(vd1126,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1619]) ).
fof(f1621,plain,
! [X0] :
( ~ rpoint(vd1124)
| vd1124 = vd1128
| ~ rline(X0)
| ~ ron(vd1124,X0)
| ~ ron(vd1126,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1620,f165]) ).
fof(f1622,plain,
! [X0] :
( ~ rpoint(vd1124)
| ~ rline(X0)
| ~ ron(vd1124,X0)
| ~ ron(vd1126,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1621,f958]) ).
fof(f1623,plain,
! [X0] :
( ~ rpoint(vd1126)
| ~ rpoint(X0)
| vd1126 = X0
| ~ rpoint(vd1124)
| ~ rline(sK4_skl(X0,vd1126))
| ~ ron(vd1124,sK4_skl(X0,vd1126)) ),
inference(resolution,[status(thm)],[f1622,f716]) ).
fof(f1626,plain,
! [X0] :
( ~ rpoint(vd1126)
| ~ rpoint(X0)
| vd1126 = X0
| ~ rpoint(vd1124)
| ~ ron(vd1124,sK4_skl(X0,vd1126)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1623,f717]) ).
fof(f1629,plain,
! [X0] :
( ~ rpoint(vd1126)
| ~ rpoint(X0)
| vd1126 = X0
| ~ ron(vd1124,sK4_skl(X0,vd1126)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1626,f169]) ).
fof(f1630,plain,
( ~ rpoint(vd1126)
| ~ rpoint(vd1124)
| vd1126 = vd1124
| ~ rpoint(vd1126)
| ~ rpoint(vd1124)
| vd1126 = vd1124 ),
inference(resolution,[status(thm)],[f1629,f715]) ).
fof(f1631,plain,
( ~ rpoint(vd1126)
| ~ rpoint(vd1124)
| vd1126 = vd1124 ),
inference(duplicate_literals_removal,[status(thm)],[f1630]) ).
fof(f1632,plain,
( ~ rpoint(vd1126)
| ~ rpoint(vd1124) ),
inference(forward_subsumption_resolution,[status(thm)],[f1631,f960]) ).
fof(f1634,plain,
~ rpoint(vd1126),
inference(forward_subsumption_resolution,[status(thm)],[f1632,f169]) ).
fof(f1635,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f167,f1634]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO284+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/10.39 % Computer : n001.cluster.edu
% 0.10/10.39 % Model : x86_64 x86_64
% 0.10/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.39 % Memory : 8046.5625MB
% 0.10/10.39 % OS : Linux 6.8.0-71-generic
% 0.10/10.40 % CPULimit : 300
% 0.10/10.40 % WCLimit : 300
% 0.10/10.40 % DateTime : Sun Sep 20 15:11:53 UTC 2026
% 0.14/10.40 % CPUTime :
% 0.14/10.43 % Drodi V4.1.1
% 0.15/10.66 % Refutation found
% 0.15/10.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/10.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/10.68 % Elapsed time: 0.272804 seconds
% 0.15/10.68 % CPU time: 1.813427 seconds
% 0.15/10.68 % Total memory used: 134.904 MB
% 0.15/10.68 % Net memory used: 132.599 MB
%------------------------------------------------------------------------------