%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO285+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 : 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:50 PM UTC 2026
% Result : Theorem 209.77s 26.95s
% Output : CNFRefutation 98.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 10
% Syntax : Number of formulae : 95 ( 38 unt; 0 def)
% Number of atoms : 278 ( 94 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 323 ( 140 ~; 129 |; 46 &)
% ( 2 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 124 ( 110 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ rinside(vd1125,vd1152),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ~ rinside(vd1125,vd1152),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
( ron(vd1123,vd1151)
& ron(vd1125,vd1151)
& rcircle(vd1152)
& rcenter(vd1123,vd1152)
& ron(vd1127,vd1152) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
vd1123 = vd1129,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,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(f18,axiom,
! [Vd1,Vd2] :
( rcenter(Vd1,Vd2)
=> ? [Vd3,Vd4] :
( rpoint(Vd3)
& Vd1 = Vd3
& rcircle(Vd4)
& Vd2 = Vd4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,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(f38,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(f39,axiom,
! [Vd713,Vd714] :
( ( rreal(Vd714)
& Vd713 = Vd714 )
=> ~ rless(Vd713,Vd713) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,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(f125,axiom,
! [Vd761,Vd762] :
( ( ? [Vd764] :
( rpoint(Vd764)
& Vd761 = Vd764 )
& ? [Vd765] :
( rpoint(Vd765)
& Vd762 = Vd765 ) )
=> vf(Vd761,Vd762) = vf(Vd762,Vd761) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f135,plain,
rinside(vd1125,vd1152),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f136,plain,
ron(vd1127,vd1152),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f137,plain,
rcenter(vd1123,vd1152),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f142,plain,
vd1123 = vd1129,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f165,plain,
rless(vf(vd1127,vd1129),vf(vd1123,vd1125)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f168,plain,
vd1130 = vd1129,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f170,plain,
vd1128 = vd1127,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f171,plain,
rpoint(vd1128),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f172,plain,
vd1125 = vd1126,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f173,plain,
rpoint(vd1126),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f174,plain,
vd1124 = vd1123,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f175,plain,
rpoint(vd1124),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f186,plain,
! [Vd1,Vd2] :
( ? [Vd3,Vd4] :
( rpoint(Vd3)
& Vd1 = Vd3
& rcircle(Vd4)
& Vd2 = Vd4 )
| ~ rcenter(Vd1,Vd2) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f187,plain,
! [Vd1,Vd2] :
( ? [Vd3] :
( rpoint(Vd3)
& Vd1 = Vd3
& ? [Vd4] :
( rcircle(Vd4)
& Vd2 = Vd4 ) )
| ~ rcenter(Vd1,Vd2) ),
inference(miniscoping,[status(thm)],[f186]) ).
fof(f188,plain,
! [Vd1,Vd2] :
( ( rpoint(sK2_skl(Vd2,Vd1))
& Vd1 = sK2_skl(Vd2,Vd1)
& rcircle(sK3_skl(Vd2,Vd1))
& Vd2 = sK3_skl(Vd2,Vd1) )
| ~ rcenter(Vd1,Vd2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(Vd3,sK2_skl(Vd2,Vd1)),skolemize(Vd4,sK3_skl(Vd2,Vd1))],[f187]) ).
fof(f191,plain,
! [X0,X1] :
( X0 = sK2_skl(X1,X0)
| ~ rcenter(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f192,plain,
! [X0,X1] :
( rpoint(sK2_skl(X1,X0))
| ~ rcenter(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f193,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)],[f19]) ).
fof(f194,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)],[f193]) ).
fof(f196,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)],[f194]) ).
fof(f257,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)],[f38]) ).
fof(f258,plain,
! [Vd741,Vd742] :
( ( rreal(sK7_skl(Vd742,Vd741))
& vf(Vd741,Vd742) = sK7_skl(Vd742,Vd741) )
| ! [Vd744] :
( ~ rpoint(Vd744)
| Vd741 != Vd744 )
| ! [Vd745] :
( ~ rpoint(Vd745)
| Vd742 != Vd745 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Vd747,sK7_skl(Vd742,Vd741))],[f257]) ).
fof(f259,plain,
! [X0,X1,X2,X3] :
( vf(X2,X0) = sK7_skl(X0,X2)
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f260,plain,
! [X0,X1,X2,X3] :
( rreal(sK7_skl(X0,X2))
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f261,plain,
! [Vd713,Vd714] :
( ~ rless(Vd713,Vd713)
| ~ rreal(Vd714)
| Vd713 != Vd714 ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f262,plain,
! [Vd713] :
( ~ rless(Vd713,Vd713)
| ! [Vd714] :
( ~ rreal(Vd714)
| Vd713 != Vd714 ) ),
inference(miniscoping,[status(thm)],[f261]) ).
fof(f263,plain,
! [X0,X1] :
( ~ rless(X0,X0)
| ~ rreal(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f264,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)],[f40]) ).
fof(f265,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)],[f264]) ).
fof(f266,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)],[f265]) ).
fof(f636,plain,
! [Vd761,Vd762] :
( vf(Vd761,Vd762) = vf(Vd762,Vd761)
| ! [Vd764] :
( ~ rpoint(Vd764)
| Vd761 != Vd764 )
| ! [Vd765] :
( ~ rpoint(Vd765)
| Vd762 != Vd765 ) ),
inference(pre_NNF_transformation,[status(thm)],[f125]) ).
fof(f637,plain,
! [X0,X1,X2,X3] :
( vf(X2,X0) = vf(X0,X2)
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f636]) ).
fof(f708,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rpoint(X0)
| vf(X0,X1) = sK7_skl(X1,X0) ),
inference(destructive_equality_resolution,[status(thm)],[f259]) ).
fof(f736,plain,
! [X0,X1,X2,X3] :
( rless(vf(X3,X1),vf(X3,X0))
| ~ ron(X0,X2)
| ~ rpoint(X1)
| ~ rcenter(X3,X2)
| ~ rinside(X1,X2)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f196]) ).
fof(f766,plain,
! [X0,X1] :
( vf(X0,X1) = vf(X1,X0)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f637]) ).
fof(f838,plain,
! [X0] :
( ~ rless(X0,X0)
| ~ rreal(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f263]) ).
fof(f849,plain,
! [X0,X1] :
( ~ rpoint(X1)
| rreal(sK7_skl(X1,X0))
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f260]) ).
fof(f891,plain,
! [X0,X1] :
( ~ rless(X0,X1)
| ~ rless(X1,X0)
| ~ rreal(X1)
| X0 = X1
| ~ rreal(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f266]) ).
fof(f913,plain,
rless(vf(vd1127,vd1130),vf(vd1123,vd1125)),
inference(backward_demodulation,[status(thm)],[f168,f165]) ).
fof(f925,plain,
rcenter(vd1124,vd1152),
inference(backward_demodulation,[status(thm)],[f174,f137]) ).
fof(f926,plain,
rless(vf(vd1127,vd1130),vf(vd1124,vd1125)),
inference(forward_demodulation,[status(thm)],[f174,f913]) ).
fof(f928,plain,
rpoint(vd1127),
inference(backward_demodulation,[status(thm)],[f170,f171]) ).
fof(f954,plain,
rpoint(sK2_skl(vd1152,vd1124)),
inference(resolution,[status(thm)],[f192,f925]) ).
fof(f961,plain,
! [X0] :
( sK7_skl(sK2_skl(vd1152,vd1124),X0) = vf(X0,sK2_skl(vd1152,vd1124))
| ~ rpoint(X0) ),
inference(resolution,[status(thm)],[f954,f708]) ).
fof(f980,plain,
vd1124 = vd1130,
inference(backward_demodulation,[status(thm)],[f981,f168]) ).
fof(f981,plain,
vd1124 = vd1129,
inference(forward_demodulation,[status(thm)],[f174,f142]) ).
fof(f1020,plain,
rpoint(vd1125),
inference(backward_demodulation,[status(thm)],[f172,f173]) ).
fof(f1140,plain,
rless(vf(vd1127,vd1124),vf(vd1124,vd1125)),
inference(backward_demodulation,[status(thm)],[f980,f926]) ).
fof(f1200,plain,
! [X0,X1] :
( ~ rpoint(X0)
| ~ ron(X1,vd1152)
| ~ rinside(X0,vd1152)
| ~ rpoint(X1)
| rless(vf(vd1124,X0),vf(vd1124,X1)) ),
inference(resolution,[status(thm)],[f736,f925]) ).
fof(f1216,plain,
! [X0] :
( ~ rpoint(vd1125)
| ~ ron(X0,vd1152)
| ~ rpoint(X0)
| rless(vf(vd1124,vd1125),vf(vd1124,X0)) ),
inference(resolution,[status(thm)],[f1200,f135]) ).
fof(f1219,plain,
! [X0] :
( rless(vf(vd1124,vd1125),vf(vd1124,X0))
| ~ rpoint(X0)
| ~ ron(X0,vd1152) ),
inference(forward_subsumption_resolution,[status(thm)],[f1216,f1020]) ).
fof(f1695,plain,
! [X0] :
( ~ rpoint(X0)
| vf(sK2_skl(vd1152,vd1124),X0) = vf(X0,sK2_skl(vd1152,vd1124)) ),
inference(resolution,[status(thm)],[f766,f954]) ).
fof(f1718,plain,
sK2_skl(vd1152,vd1124) = vd1124,
inference(resolution,[status(thm)],[f191,f925]) ).
fof(f1742,plain,
! [X0] :
( sK7_skl(sK2_skl(vd1152,vd1124),X0) = vf(X0,vd1124)
| ~ rpoint(X0) ),
inference(backward_demodulation,[status(thm)],[f1718,f961]) ).
fof(f1770,plain,
! [X0] :
( sK7_skl(vd1124,X0) = vf(X0,vd1124)
| ~ rpoint(X0) ),
inference(forward_demodulation,[status(thm)],[f1718,f1742]) ).
fof(f4341,plain,
! [X0] :
( ~ rpoint(X0)
| vf(vd1124,X0) = vf(X0,sK2_skl(vd1152,vd1124)) ),
inference(forward_demodulation,[status(thm)],[f1718,f1695]) ).
fof(f4342,plain,
! [X0] :
( vf(vd1124,X0) = vf(X0,vd1124)
| ~ rpoint(X0) ),
inference(forward_demodulation,[status(thm)],[f1718,f4341]) ).
fof(f4368,plain,
vf(vd1125,vd1124) = vf(vd1124,vd1125),
inference(resolution,[status(thm)],[f4342,f1020]) ).
fof(f4369,plain,
vf(vd1124,vd1127) = vf(vd1127,vd1124),
inference(resolution,[status(thm)],[f4342,f928]) ).
fof(f6529,plain,
( sK7_skl(vd1124,vd1125) = vf(vd1124,vd1125)
| ~ rpoint(vd1125) ),
inference(paramodulation,[status(thm)],[f4368,f1770]) ).
fof(f6531,plain,
vf(vd1124,vd1125) = sK7_skl(vd1124,vd1125),
inference(forward_subsumption_resolution,[status(thm)],[f6529,f1020]) ).
fof(f6777,plain,
rless(vf(vd1124,vd1127),vf(vd1124,vd1125)),
inference(backward_demodulation,[status(thm)],[f4369,f1140]) ).
fof(f6778,plain,
( sK7_skl(vd1124,vd1127) = vf(vd1124,vd1127)
| ~ rpoint(vd1127) ),
inference(paramodulation,[status(thm)],[f4369,f1770]) ).
fof(f6780,plain,
sK7_skl(vd1124,vd1127) = vf(vd1124,vd1127),
inference(forward_subsumption_resolution,[status(thm)],[f6778,f928]) ).
fof(f8155,plain,
rless(vf(vd1124,vd1127),sK7_skl(vd1124,vd1125)),
inference(backward_demodulation,[status(thm)],[f6531,f6777]) ).
fof(f8157,plain,
! [X0] :
( ~ ron(X0,vd1152)
| rless(sK7_skl(vd1124,vd1125),vf(vd1124,X0))
| ~ rpoint(X0) ),
inference(backward_demodulation,[status(thm)],[f6531,f1219]) ).
fof(f8181,plain,
rless(sK7_skl(vd1124,vd1127),sK7_skl(vd1124,vd1125)),
inference(backward_demodulation,[status(thm)],[f6780,f8155]) ).
fof(f8235,plain,
( ~ rreal(sK7_skl(vd1124,vd1127))
| sK7_skl(vd1124,vd1127) = sK7_skl(vd1124,vd1125)
| ~ rless(sK7_skl(vd1124,vd1125),sK7_skl(vd1124,vd1127))
| ~ rreal(sK7_skl(vd1124,vd1125)) ),
inference(resolution,[status(thm)],[f8181,f891]) ).
fof(f8243,plain,
( rless(sK7_skl(vd1124,vd1125),vf(vd1124,vd1127))
| ~ rpoint(vd1127) ),
inference(resolution,[status(thm)],[f8157,f136]) ).
fof(f8249,plain,
( rless(sK7_skl(vd1124,vd1125),sK7_skl(vd1124,vd1127))
| ~ rpoint(vd1127) ),
inference(forward_demodulation,[status(thm)],[f6780,f8243]) ).
fof(f8250,plain,
rless(sK7_skl(vd1124,vd1125),sK7_skl(vd1124,vd1127)),
inference(forward_subsumption_resolution,[status(thm)],[f8249,f928]) ).
fof(f8335,plain,
( ~ rreal(sK7_skl(vd1124,vd1127))
| sK7_skl(vd1124,vd1127) = sK7_skl(vd1124,vd1125)
| ~ rreal(sK7_skl(vd1124,vd1125)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8235,f8250]) ).
fof(f8336,plain,
( ~ rpoint(vd1124)
| ~ rpoint(vd1125)
| ~ rreal(sK7_skl(vd1124,vd1127))
| sK7_skl(vd1124,vd1127) = sK7_skl(vd1124,vd1125) ),
inference(resolution,[status(thm)],[f8335,f849]) ).
fof(f8337,plain,
( ~ rreal(sK7_skl(vd1124,vd1127))
| ~ rpoint(vd1124)
| sK7_skl(vd1124,vd1125) = sK7_skl(vd1124,vd1127) ),
inference(forward_subsumption_resolution,[status(thm)],[f8336,f1020]) ).
fof(f8356,plain,
( ~ rreal(sK7_skl(vd1124,vd1127))
| sK7_skl(vd1124,vd1125) = sK7_skl(vd1124,vd1127) ),
inference(forward_subsumption_resolution,[status(thm)],[f8337,f175]) ).
fof(f8357,plain,
( ~ rpoint(vd1124)
| ~ rpoint(vd1127)
| sK7_skl(vd1124,vd1125) = sK7_skl(vd1124,vd1127) ),
inference(resolution,[status(thm)],[f8356,f849]) ).
fof(f8358,plain,
( ~ rpoint(vd1124)
| sK7_skl(vd1124,vd1125) = sK7_skl(vd1124,vd1127) ),
inference(forward_subsumption_resolution,[status(thm)],[f8357,f928]) ).
fof(f9713,plain,
rless(sK7_skl(vd1124,vd1127),sK7_skl(vd1124,vd1127)),
inference(backward_demodulation,[status(thm)],[f9716,f8181]) ).
fof(f9716,plain,
sK7_skl(vd1124,vd1127) = sK7_skl(vd1124,vd1125),
inference(forward_subsumption_resolution,[status(thm)],[f8358,f175]) ).
fof(f9717,plain,
( ~ rpoint(vd1124)
| rreal(sK7_skl(vd1124,vd1127))
| ~ rpoint(vd1125) ),
inference(paramodulation,[status(thm)],[f9716,f849]) ).
fof(f9720,plain,
( ~ rpoint(vd1124)
| rreal(sK7_skl(vd1124,vd1127)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9717,f1020]) ).
fof(f9786,plain,
rreal(sK7_skl(vd1124,vd1127)),
inference(forward_subsumption_resolution,[status(thm)],[f9720,f175]) ).
fof(f9799,plain,
~ rless(sK7_skl(vd1124,vd1127),sK7_skl(vd1124,vd1127)),
inference(resolution,[status(thm)],[f9786,f838]) ).
fof(f9801,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f9799,f9713]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO285+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % 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 15:11:57 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.40 % Drodi V4.1.1
% 209.77/26.95 % Refutation found
% 209.77/26.95 % SZS status Theorem for theBenchmark: Theorem is valid
% 209.77/26.95 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 13.31/27.00 % Elapsed time: 26.616459 seconds
% 13.31/27.00 % CPU time: 210.822801 seconds
% 13.31/27.00 % Total memory used: 520.818 MB
% 13.31/27.00 % Net memory used: 483.611 MB
%------------------------------------------------------------------------------