%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO280+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 12:24:49 PM UTC 2026
% Result : Theorem 271.73s 44.99s
% Output : CNFRefutation 138.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 9
% Syntax : Number of formulae : 82 ( 37 unt; 0 def)
% Number of atoms : 240 ( 71 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 290 ( 132 ~; 121 |; 31 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 88 ( 82 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ rinside(vd1125,vd1139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ~ rinside(vd1125,vd1139),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
( ron(vd1123,vd1138)
& ron(vd1125,vd1138)
& rcircle(vd1139)
& rcenter(vd1123,vd1139)
& ron(vd1136,vd1139) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
vf(vd1127,vd1129) = vf(vd1123,vd1136),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
rpoint(vd1136),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,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/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [Vd741,Vd742] :
( ( ? [Vd744] :
( rpoint(Vd744)
& Vd741 = Vd744 )
& ? [Vd745] :
( rpoint(Vd745)
& Vd742 = Vd745 ) )
=> ? [Vd747] :
( rreal(Vd747)
& vf(Vd741,Vd742) = Vd747 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [Vd854,Vd855,Vd859,Vd860] :
( ( ? [Vd857] :
( rpoint(Vd857)
& Vd854 = Vd857 )
& ? [Vd858] :
( rpoint(Vd858)
& Vd855 = Vd858 )
& rcenter(Vd859,Vd860)
& ron(Vd855,Vd860) )
=> ( rless(vf(Vd859,Vd854),vf(Vd859,Vd855))
<=> rinside(Vd854,Vd860) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [Vd713,Vd714] :
( ( rreal(Vd714)
& Vd713 = Vd714 )
=> ~ rless(Vd713,Vd713) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [Vd706,Vd707,Vd708,Vd709] :
( ( rreal(Vd707)
& Vd706 = Vd707
& rreal(Vd709)
& Vd708 = Vd709
& rless(Vd706,Vd708) )
=> ( Vd706 = Vd708
| ~ rless(Vd708,Vd706) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f117,plain,
rinside(vd1125,vd1139),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f118,plain,
ron(vd1136,vd1139),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f119,plain,
rcenter(vd1123,vd1139),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f124,plain,
vf(vd1127,vd1129) = vf(vd1123,vd1136),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f125,plain,
rpoint(vd1136),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f126,plain,
rless(vf(vd1127,vd1129),vf(vd1123,vd1125)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f129,plain,
vd1129 = vd1130,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f130,plain,
rpoint(vd1130),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f131,plain,
vd1127 = vd1128,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f132,plain,
rpoint(vd1128),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f133,plain,
vd1125 = vd1126,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f134,plain,
rpoint(vd1126),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f135,plain,
vd1123 = vd1124,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f136,plain,
rpoint(vd1124),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f197,plain,
! [Vd741,Vd742] :
( ? [Vd747] :
( rreal(Vd747)
& vf(Vd741,Vd742) = Vd747 )
| ! [Vd744] :
( ~ rpoint(Vd744)
| Vd741 != Vd744 )
| ! [Vd745] :
( ~ rpoint(Vd745)
| Vd742 != Vd745 ) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f198,plain,
! [Vd741,Vd742] :
( ( rreal(sK5_skl(Vd742,Vd741))
& vf(Vd741,Vd742) = sK5_skl(Vd742,Vd741) )
| ! [Vd744] :
( ~ rpoint(Vd744)
| Vd741 != Vd744 )
| ! [Vd745] :
( ~ rpoint(Vd745)
| Vd742 != Vd745 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(Vd747,sK5_skl(Vd742,Vd741))],[f197]) ).
fof(f199,plain,
! [X0,X1,X2,X3] :
( vf(X2,X0) = sK5_skl(X0,X2)
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f200,plain,
! [X0,X1,X2,X3] :
( rreal(sK5_skl(X0,X2))
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f198]) ).
fof(f219,plain,
! [Vd854,Vd855,Vd859,Vd860] :
( ( rless(vf(Vd859,Vd854),vf(Vd859,Vd855))
<=> rinside(Vd854,Vd860) )
| ! [Vd857] :
( ~ rpoint(Vd857)
| Vd854 != Vd857 )
| ! [Vd858] :
( ~ rpoint(Vd858)
| Vd855 != Vd858 )
| ~ rcenter(Vd859,Vd860)
| ~ ron(Vd855,Vd860) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f220,plain,
! [Vd854,Vd855,Vd859,Vd860] :
( ( ( ~ rinside(Vd854,Vd860)
| rless(vf(Vd859,Vd854),vf(Vd859,Vd855)) )
& ( rinside(Vd854,Vd860)
| ~ rless(vf(Vd859,Vd854),vf(Vd859,Vd855)) ) )
| ! [Vd857] :
( ~ rpoint(Vd857)
| Vd854 != Vd857 )
| ! [Vd858] :
( ~ rpoint(Vd858)
| Vd855 != Vd858 )
| ~ rcenter(Vd859,Vd860)
| ~ ron(Vd855,Vd860) ),
inference(NNF_transformation,[status(thm)],[f219]) ).
fof(f222,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ rinside(X4,X1)
| rless(vf(X2,X4),vf(X2,X0))
| ~ rpoint(X5)
| X4 != X5
| ~ rpoint(X3)
| X0 != X3
| ~ rcenter(X2,X1)
| ~ ron(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f229,plain,
! [Vd713,Vd714] :
( ~ rless(Vd713,Vd713)
| ~ rreal(Vd714)
| Vd713 != Vd714 ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f230,plain,
! [Vd713] :
( ~ rless(Vd713,Vd713)
| ! [Vd714] :
( ~ rreal(Vd714)
| Vd713 != Vd714 ) ),
inference(miniscoping,[status(thm)],[f229]) ).
fof(f231,plain,
! [X0,X1] :
( ~ rless(X0,X0)
| ~ rreal(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f232,plain,
! [Vd706,Vd707,Vd708,Vd709] :
( Vd706 = Vd708
| ~ rless(Vd708,Vd706)
| ~ rreal(Vd707)
| Vd706 != Vd707
| ~ rreal(Vd709)
| Vd708 != Vd709
| ~ rless(Vd706,Vd708) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f233,plain,
! [Vd706,Vd708] :
( Vd706 = Vd708
| ~ rless(Vd708,Vd706)
| ! [Vd707] :
( ~ rreal(Vd707)
| Vd706 != Vd707
| ! [Vd709] :
( ~ rreal(Vd709)
| Vd708 != Vd709
| ~ rless(Vd706,Vd708) ) ) ),
inference(miniscoping,[status(thm)],[f232]) ).
fof(f234,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ rless(X1,X0)
| ~ rreal(X3)
| X0 != X3
| ~ rreal(X2)
| X1 != X2
| ~ rless(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f233]) ).
fof(f661,plain,
! [X0,X1] :
( vf(X1,X0) = sK5_skl(X0,X1)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f199]) ).
fof(f662,plain,
! [X0,X1] :
( rreal(sK5_skl(X0,X1))
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f200]) ).
fof(f671,plain,
! [X0,X1,X2,X3] :
( ~ rinside(X3,X1)
| rless(vf(X2,X3),vf(X2,X0))
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rcenter(X2,X1)
| ~ ron(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f222]) ).
fof(f674,plain,
! [X0] :
( ~ rless(X0,X0)
| ~ rreal(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f231]) ).
fof(f675,plain,
! [X0,X1] :
( X0 = X1
| ~ rless(X1,X0)
| ~ rreal(X0)
| ~ rreal(X1)
| ~ rless(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f234]) ).
fof(f866,plain,
rpoint(vd1129),
inference(forward_demodulation,[status(thm)],[f129,f130]) ).
fof(f878,plain,
rpoint(vd1127),
inference(forward_demodulation,[status(thm)],[f131,f132]) ).
fof(f890,plain,
rpoint(vd1125),
inference(forward_demodulation,[status(thm)],[f133,f134]) ).
fof(f902,plain,
rpoint(vd1123),
inference(forward_demodulation,[status(thm)],[f135,f136]) ).
fof(f937,plain,
rless(vf(vd1123,vd1136),vf(vd1123,vd1125)),
inference(backward_demodulation,[status(thm)],[f124,f126]) ).
fof(f3334,plain,
! [X0] :
( vf(vd1123,X0) = sK5_skl(X0,vd1123)
| ~ rpoint(X0) ),
inference(resolution,[status(thm)],[f661,f902]) ).
fof(f3336,plain,
! [X0] :
( vf(vd1127,X0) = sK5_skl(X0,vd1127)
| ~ rpoint(X0) ),
inference(resolution,[status(thm)],[f661,f878]) ).
fof(f3998,plain,
! [X0,X1] :
( ~ rinside(X1,vd1139)
| rless(vf(vd1123,X1),vf(vd1123,X0))
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ ron(X0,vd1139) ),
inference(resolution,[status(thm)],[f671,f119]) ).
fof(f4153,plain,
( vf(vd1123,vd1125) = vf(vd1123,vd1136)
| ~ rreal(vf(vd1123,vd1125))
| ~ rreal(vf(vd1123,vd1136))
| ~ rless(vf(vd1123,vd1125),vf(vd1123,vd1136)) ),
inference(resolution,[status(thm)],[f675,f937]) ).
fof(f4802,plain,
! [X0] :
( rless(vf(vd1123,vd1125),vf(vd1123,X0))
| ~ rpoint(vd1125)
| ~ rpoint(X0)
| ~ ron(X0,vd1139) ),
inference(resolution,[status(thm)],[f3998,f117]) ).
fof(f4806,plain,
! [X0] :
( rless(vf(vd1123,vd1125),vf(vd1123,X0))
| ~ rpoint(X0)
| ~ ron(X0,vd1139) ),
inference(forward_subsumption_resolution,[status(thm)],[f4802,f890]) ).
fof(f5511,plain,
vf(vd1123,vd1125) = sK5_skl(vd1125,vd1123),
inference(resolution,[status(thm)],[f3334,f890]) ).
fof(f5514,plain,
vf(vd1123,vd1136) = sK5_skl(vd1136,vd1123),
inference(resolution,[status(thm)],[f3334,f125]) ).
fof(f5526,plain,
( sK5_skl(vd1125,vd1123) = vf(vd1123,vd1136)
| ~ rreal(vf(vd1123,vd1125))
| ~ rreal(vf(vd1123,vd1136))
| ~ rless(vf(vd1123,vd1125),vf(vd1123,vd1136)) ),
inference(backward_demodulation,[status(thm)],[f5511,f4153]) ).
fof(f5530,plain,
! [X0] :
( rless(sK5_skl(vd1125,vd1123),vf(vd1123,X0))
| ~ rpoint(X0)
| ~ ron(X0,vd1139) ),
inference(backward_demodulation,[status(thm)],[f5511,f4806]) ).
fof(f5533,plain,
rless(vf(vd1123,vd1136),sK5_skl(vd1125,vd1123)),
inference(backward_demodulation,[status(thm)],[f5511,f937]) ).
fof(f5537,plain,
( sK5_skl(vd1125,vd1123) = vf(vd1123,vd1136)
| ~ rreal(vf(vd1123,vd1125))
| ~ rreal(vf(vd1123,vd1136))
| ~ rless(sK5_skl(vd1125,vd1123),vf(vd1123,vd1136)) ),
inference(forward_demodulation,[status(thm)],[f5511,f5526]) ).
fof(f5538,plain,
( sK5_skl(vd1125,vd1123) = vf(vd1123,vd1136)
| ~ rreal(sK5_skl(vd1125,vd1123))
| ~ rreal(vf(vd1123,vd1136))
| ~ rless(sK5_skl(vd1125,vd1123),vf(vd1123,vd1136)) ),
inference(forward_demodulation,[status(thm)],[f5511,f5537]) ).
fof(f5558,plain,
vf(vd1127,vd1129) = sK5_skl(vd1136,vd1123),
inference(backward_demodulation,[status(thm)],[f5514,f124]) ).
fof(f5596,plain,
( rless(sK5_skl(vd1125,vd1123),vf(vd1123,vd1136))
| ~ rpoint(vd1136) ),
inference(resolution,[status(thm)],[f5530,f118]) ).
fof(f5604,plain,
( rless(sK5_skl(vd1125,vd1123),sK5_skl(vd1136,vd1123))
| ~ rpoint(vd1136) ),
inference(forward_demodulation,[status(thm)],[f5514,f5596]) ).
fof(f5605,plain,
rless(sK5_skl(vd1125,vd1123),sK5_skl(vd1136,vd1123)),
inference(forward_subsumption_resolution,[status(thm)],[f5604,f125]) ).
fof(f5627,plain,
rless(sK5_skl(vd1136,vd1123),sK5_skl(vd1125,vd1123)),
inference(forward_demodulation,[status(thm)],[f5514,f5533]) ).
fof(f5693,plain,
( sK5_skl(vd1125,vd1123) = vf(vd1123,vd1136)
| ~ rreal(sK5_skl(vd1125,vd1123))
| ~ rreal(vf(vd1123,vd1136))
| ~ rless(sK5_skl(vd1125,vd1123),sK5_skl(vd1136,vd1123)) ),
inference(forward_demodulation,[status(thm)],[f5514,f5538]) ).
fof(f5694,plain,
( sK5_skl(vd1125,vd1123) = vf(vd1123,vd1136)
| ~ rreal(sK5_skl(vd1125,vd1123))
| ~ rreal(sK5_skl(vd1136,vd1123))
| ~ rless(sK5_skl(vd1125,vd1123),sK5_skl(vd1136,vd1123)) ),
inference(forward_demodulation,[status(thm)],[f5514,f5693]) ).
fof(f5695,plain,
( sK5_skl(vd1125,vd1123) = sK5_skl(vd1136,vd1123)
| ~ rreal(sK5_skl(vd1125,vd1123))
| ~ rreal(sK5_skl(vd1136,vd1123))
| ~ rless(sK5_skl(vd1125,vd1123),sK5_skl(vd1136,vd1123)) ),
inference(forward_demodulation,[status(thm)],[f5514,f5694]) ).
fof(f5696,plain,
( sK5_skl(vd1125,vd1123) = sK5_skl(vd1136,vd1123)
| ~ rreal(sK5_skl(vd1125,vd1123))
| ~ rreal(sK5_skl(vd1136,vd1123)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5695,f5605]) ).
fof(f5838,plain,
vf(vd1127,vd1129) = sK5_skl(vd1129,vd1127),
inference(resolution,[status(thm)],[f3336,f866]) ).
fof(f5841,plain,
sK5_skl(vd1136,vd1123) = sK5_skl(vd1129,vd1127),
inference(forward_demodulation,[status(thm)],[f5558,f5838]) ).
fof(f5850,plain,
( rreal(sK5_skl(vd1136,vd1123))
| ~ rpoint(vd1127)
| ~ rpoint(vd1129) ),
inference(paramodulation,[status(thm)],[f5841,f662]) ).
fof(f5851,plain,
( rreal(sK5_skl(vd1136,vd1123))
| ~ rpoint(vd1127) ),
inference(forward_subsumption_resolution,[status(thm)],[f5850,f866]) ).
fof(f5855,plain,
( sK5_skl(vd1125,vd1123) = sK5_skl(vd1136,vd1123)
| ~ rreal(sK5_skl(vd1125,vd1123)) ),
inference(backward_subsumption_resolution,[status(thm)],[f5696,f5856]) ).
fof(f5856,plain,
rreal(sK5_skl(vd1136,vd1123)),
inference(forward_subsumption_resolution,[status(thm)],[f5851,f878]) ).
fof(f5930,plain,
( ~ rpoint(vd1123)
| ~ rpoint(vd1125)
| sK5_skl(vd1125,vd1123) = sK5_skl(vd1136,vd1123) ),
inference(resolution,[status(thm)],[f5855,f662]) ).
fof(f5931,plain,
( ~ rpoint(vd1123)
| sK5_skl(vd1125,vd1123) = sK5_skl(vd1136,vd1123) ),
inference(forward_subsumption_resolution,[status(thm)],[f5930,f890]) ).
fof(f5933,plain,
rreal(sK5_skl(vd1125,vd1123)),
inference(backward_demodulation,[status(thm)],[f5939,f5856]) ).
fof(f5936,plain,
rless(sK5_skl(vd1125,vd1123),sK5_skl(vd1125,vd1123)),
inference(backward_demodulation,[status(thm)],[f5939,f5627]) ).
fof(f5939,plain,
sK5_skl(vd1125,vd1123) = sK5_skl(vd1136,vd1123),
inference(forward_subsumption_resolution,[status(thm)],[f5931,f902]) ).
fof(f5962,plain,
~ rreal(sK5_skl(vd1125,vd1123)),
inference(resolution,[status(thm)],[f5936,f674]) ).
fof(f5965,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f5962,f5933]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GEO280+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/10.44 % Computer : n006.cluster.edu
% 0.17/10.44 % Model : x86_64 x86_64
% 0.17/10.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/10.44 % Memory : 8046.5625MB
% 0.17/10.44 % OS : Linux 6.8.0-71-generic
% 0.17/10.44 % CPULimit : 300
% 0.17/10.44 % WCLimit : 300
% 0.17/10.44 % DateTime : Sun Sep 20 15:04:09 UTC 2026
% 0.17/10.44 % CPUTime :
% 0.17/10.48 % Drodi V4.1.1
% 271.73/44.99 % Refutation found
% 271.73/44.99 % SZS status Theorem for theBenchmark: Theorem is valid
% 271.73/44.99 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 138.42/45.04 % Elapsed time: 34.575015 seconds
% 138.42/45.04 % CPU time: 272.615561 seconds
% 138.42/45.04 % Total memory used: 432.601 MB
% 138.42/45.04 % Net memory used: 392.119 MB
%------------------------------------------------------------------------------