%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO282+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 : n011.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 159.87s 20.65s
% Output : CNFRefutation 159.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 8
% Syntax : Number of formulae : 64 ( 28 unt; 0 def)
% Number of atoms : 200 ( 59 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 246 ( 110 ~; 99 |; 31 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 86 ( 80 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ rinside(vd1125,vd1146),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ~ rinside(vd1125,vd1146),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
( ron(vd1123,vd1145)
& ron(vd1125,vd1145)
& rcircle(vd1146)
& rcenter(vd1123,vd1146)
& ron(vd1129,vd1146) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
vd1123 = vd1127,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,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(f21,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [Vd741,Vd742] :
( ( ? [Vd744] :
( rpoint(Vd744)
& Vd741 = Vd744 )
& ? [Vd745] :
( rpoint(Vd745)
& Vd742 = Vd745 ) )
=> ? [Vd747] :
( rreal(Vd747)
& vf(Vd741,Vd742) = Vd747 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [Vd713,Vd714] :
( ( rreal(Vd714)
& Vd713 = Vd714 )
=> ~ rless(Vd713,Vd713) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [Vd706,Vd707,Vd708,Vd709] :
( ( rreal(Vd707)
& Vd706 = Vd707
& rreal(Vd709)
& Vd708 = Vd709
& rless(Vd706,Vd708) )
=> ( Vd706 = Vd708
| ~ rless(Vd708,Vd706) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f126,plain,
rinside(vd1125,vd1146),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f127,plain,
ron(vd1129,vd1146),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f128,plain,
rcenter(vd1123,vd1146),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f133,plain,
vd1123 = vd1127,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f162,plain,
rless(vf(vd1127,vd1129),vf(vd1123,vd1125)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f165,plain,
vd1129 = vd1130,
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f166,plain,
rpoint(vd1130),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f167,plain,
vd1127 = vd1128,
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f168,plain,
rpoint(vd1128),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f169,plain,
vd1125 = vd1126,
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f170,plain,
rpoint(vd1126),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f183,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)],[f21]) ).
fof(f184,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)],[f183]) ).
fof(f186,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)],[f184]) ).
fof(f192,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)],[f23]) ).
fof(f193,plain,
! [Vd741,Vd742] :
( ( rreal(sK2_skl(Vd742,Vd741))
& vf(Vd741,Vd742) = sK2_skl(Vd742,Vd741) )
| ! [Vd744] :
( ~ rpoint(Vd744)
| Vd741 != Vd744 )
| ! [Vd745] :
( ~ rpoint(Vd745)
| Vd742 != Vd745 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Vd747,sK2_skl(Vd742,Vd741))],[f192]) ).
fof(f194,plain,
! [X0,X1,X2,X3] :
( vf(X2,X0) = sK2_skl(X0,X2)
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f195,plain,
! [X0,X1,X2,X3] :
( rreal(sK2_skl(X0,X2))
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f196,plain,
! [Vd713,Vd714] :
( ~ rless(Vd713,Vd713)
| ~ rreal(Vd714)
| Vd713 != Vd714 ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f197,plain,
! [Vd713] :
( ~ rless(Vd713,Vd713)
| ! [Vd714] :
( ~ rreal(Vd714)
| Vd713 != Vd714 ) ),
inference(miniscoping,[status(thm)],[f196]) ).
fof(f198,plain,
! [X0,X1] :
( ~ rless(X0,X0)
| ~ rreal(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f199,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)],[f25]) ).
fof(f200,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)],[f199]) ).
fof(f201,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)],[f200]) ).
fof(f675,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)],[f186]) ).
fof(f678,plain,
! [X0,X1] :
( vf(X1,X0) = sK2_skl(X0,X1)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f194]) ).
fof(f679,plain,
! [X0,X1] :
( rreal(sK2_skl(X0,X1))
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f195]) ).
fof(f680,plain,
! [X0] :
( ~ rless(X0,X0)
| ~ rreal(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f198]) ).
fof(f681,plain,
! [X0,X1] :
( X0 = X1
| ~ rless(X1,X0)
| ~ rreal(X0)
| ~ rreal(X1)
| ~ rless(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f201]) ).
fof(f889,plain,
rless(vf(vd1123,vd1129),vf(vd1123,vd1125)),
inference(backward_demodulation,[status(thm)],[f133,f162]) ).
fof(f891,plain,
rpoint(vd1129),
inference(forward_demodulation,[status(thm)],[f165,f166]) ).
fof(f899,plain,
vd1123 = vd1128,
inference(forward_demodulation,[status(thm)],[f133,f167]) ).
fof(f900,plain,
rpoint(vd1123),
inference(forward_demodulation,[status(thm)],[f899,f168]) ).
fof(f908,plain,
rpoint(vd1125),
inference(forward_demodulation,[status(thm)],[f169,f170]) ).
fof(f1156,plain,
! [X0,X1] :
( ~ rinside(X1,vd1146)
| rless(vf(vd1123,X1),vf(vd1123,X0))
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ ron(X0,vd1146) ),
inference(resolution,[status(thm)],[f675,f128]) ).
fof(f1163,plain,
! [X0] :
( ~ rinside(X0,vd1146)
| rless(vf(vd1123,X0),vf(vd1123,vd1129))
| ~ rpoint(X0)
| ~ rpoint(vd1129) ),
inference(resolution,[status(thm)],[f1156,f127]) ).
fof(f1165,plain,
! [X0] :
( ~ rinside(X0,vd1146)
| rless(vf(vd1123,X0),vf(vd1123,vd1129))
| ~ rpoint(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1163,f891]) ).
fof(f1208,plain,
! [X0] :
( vf(vd1123,X0) = sK2_skl(X0,vd1123)
| ~ rpoint(X0) ),
inference(resolution,[status(thm)],[f678,f900]) ).
fof(f1237,plain,
( vf(vd1123,vd1125) = vf(vd1123,vd1129)
| ~ rreal(vf(vd1123,vd1125))
| ~ rreal(vf(vd1123,vd1129))
| ~ rless(vf(vd1123,vd1125),vf(vd1123,vd1129)) ),
inference(resolution,[status(thm)],[f681,f889]) ).
fof(f2196,plain,
( rless(vf(vd1123,vd1125),vf(vd1123,vd1129))
| ~ rpoint(vd1125) ),
inference(resolution,[status(thm)],[f1165,f126]) ).
fof(f2200,plain,
rless(vf(vd1123,vd1125),vf(vd1123,vd1129)),
inference(forward_subsumption_resolution,[status(thm)],[f2196,f908]) ).
fof(f2674,plain,
( vf(vd1123,vd1125) = vf(vd1123,vd1129)
| ~ rreal(vf(vd1123,vd1125))
| ~ rreal(vf(vd1123,vd1129)) ),
inference(backward_subsumption_resolution,[status(thm)],[f1237,f2200]) ).
fof(f17572,plain,
vf(vd1123,vd1125) = sK2_skl(vd1125,vd1123),
inference(resolution,[status(thm)],[f1208,f908]) ).
fof(f17574,plain,
vf(vd1123,vd1129) = sK2_skl(vd1129,vd1123),
inference(resolution,[status(thm)],[f1208,f891]) ).
fof(f17581,plain,
( rreal(vf(vd1123,vd1125))
| ~ rpoint(vd1123)
| ~ rpoint(vd1125) ),
inference(paramodulation,[status(thm)],[f17572,f679]) ).
fof(f17582,plain,
( rreal(vf(vd1123,vd1125))
| ~ rpoint(vd1123) ),
inference(forward_subsumption_resolution,[status(thm)],[f17581,f908]) ).
fof(f17589,plain,
( rreal(vf(vd1123,vd1129))
| ~ rpoint(vd1123)
| ~ rpoint(vd1129) ),
inference(paramodulation,[status(thm)],[f17574,f679]) ).
fof(f17590,plain,
( rreal(vf(vd1123,vd1129))
| ~ rpoint(vd1123) ),
inference(forward_subsumption_resolution,[status(thm)],[f17589,f891]) ).
fof(f17599,plain,
( vf(vd1123,vd1125) = vf(vd1123,vd1129)
| ~ rreal(vf(vd1123,vd1129)) ),
inference(backward_subsumption_resolution,[status(thm)],[f2674,f17600]) ).
fof(f17600,plain,
rreal(vf(vd1123,vd1125)),
inference(forward_subsumption_resolution,[status(thm)],[f17582,f900]) ).
fof(f17608,plain,
rreal(vf(vd1123,vd1129)),
inference(forward_subsumption_resolution,[status(thm)],[f17590,f900]) ).
fof(f17844,plain,
rless(vf(vd1123,vd1125),vf(vd1123,vd1125)),
inference(backward_demodulation,[status(thm)],[f17845,f889]) ).
fof(f17845,plain,
vf(vd1123,vd1125) = vf(vd1123,vd1129),
inference(forward_subsumption_resolution,[status(thm)],[f17599,f17608]) ).
fof(f17851,plain,
~ rreal(vf(vd1123,vd1125)),
inference(resolution,[status(thm)],[f17844,f680]) ).
fof(f17852,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f17851,f17600]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO282+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n011.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 15:05:10 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 159.87/20.65 % Refutation found
% 159.87/20.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 159.87/20.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.21/20.89 % Elapsed time: 20.522917 seconds
% 10.21/20.89 % CPU time: 160.706635 seconds
% 10.21/20.89 % Total memory used: 390.562 MB
% 10.21/20.89 % Net memory used: 361.481 MB
%------------------------------------------------------------------------------