%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO336+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 : n003.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:55 PM UTC 2026
% Result : Theorem 3.27s 0.90s
% Output : CNFRefutation 3.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 25
% Syntax : Number of formulae : 122 ( 36 unt; 12 def)
% Number of atoms : 408 ( 146 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 500 ( 214 ~; 208 |; 60 &)
% ( 12 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 13 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-8 aty)
% Number of variables : 151 ( 138 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
? [Vd1378] :
( rpoint(Vd1378)
& rR(Vd1378,vd1361,vd1363)
& vf(vd1363,Vd1378) = vf(vd1361,vd1362) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ? [Vd1378] :
( rpoint(Vd1378)
& rR(Vd1378,vd1361,vd1363)
& vf(vd1363,Vd1378) = vf(vd1361,vd1362) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
rless(vf(vd1361,vd1362),vf(vd1361,vd1363)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116] :
( ( rpoint(Vd1110)
& Vd1109 = Vd1110
& rpoint(Vd1112)
& Vd1111 = Vd1112
& rpoint(Vd1114)
& Vd1113 = Vd1114
& rpoint(Vd1116)
& Vd1115 = Vd1116
& Vd1109 != Vd1111
& Vd1113 != Vd1115
& rless(vf(Vd1113,Vd1115),vf(Vd1109,Vd1111)) )
=> vf(Vd1109,vskolem1120(Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116)) = vf(Vd1113,Vd1115) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116] :
( ( rpoint(Vd1110)
& Vd1109 = Vd1110
& rpoint(Vd1112)
& Vd1111 = Vd1112
& rpoint(Vd1114)
& Vd1113 = Vd1114
& rpoint(Vd1116)
& Vd1115 = Vd1116
& Vd1109 != Vd1111
& Vd1113 != Vd1115
& rless(vf(Vd1113,Vd1115),vf(Vd1109,Vd1111)) )
=> rR(vskolem1120(Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116),Vd1109,Vd1111) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116] :
( ( rpoint(Vd1110)
& Vd1109 = Vd1110
& rpoint(Vd1112)
& Vd1111 = Vd1112
& rpoint(Vd1114)
& Vd1113 = Vd1114
& rpoint(Vd1116)
& Vd1115 = Vd1116
& Vd1109 != Vd1111
& Vd1113 != Vd1115
& rless(vf(Vd1113,Vd1115),vf(Vd1109,Vd1111)) )
=> rpoint(vskolem1120(Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
? [Vd1367] :
( rpoint(Vd1367)
& vd1362 = Vd1367 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [Vd761,Vd762] :
( ( ? [Vd764] :
( rpoint(Vd764)
& Vd761 = Vd764 )
& ? [Vd765] :
( rpoint(Vd765)
& Vd762 = Vd765 ) )
=> vf(Vd761,Vd762) = vf(Vd762,Vd761) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [Vd340,Vd341,Vd342] :
( ( ? [Vd344] :
( rpoint(Vd344)
& Vd340 = Vd344 )
& ? [Vd345] :
( rpoint(Vd345)
& Vd341 = Vd345 )
& ? [Vd346] :
( rpoint(Vd346)
& Vd342 = Vd346 )
& rR(Vd341,Vd340,Vd342) )
=> ( rR(Vd341,Vd342,Vd340)
& Vd340 != Vd341
& Vd340 != Vd342
& ~ rR(Vd340,Vd341,Vd342) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
vd1361 != vd1363,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
vd1361 != vd1362,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
? [Vd1368] :
( rpoint(Vd1368)
& vd1363 = Vd1368 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
? [Vd1366] :
( rpoint(Vd1366)
& vd1361 = Vd1366 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f110,axiom,
! [Vd15,Vd16] :
( ( rpoint(Vd16)
& Vd15 = Vd16 )
=> ? [Vd17] :
( rpoint(Vd17)
& Vd17 != Vd15 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,plain,
! [Vd1378] :
( ~ rpoint(Vd1378)
| ~ rR(Vd1378,vd1361,vd1363)
| vf(vd1363,Vd1378) != vf(vd1361,vd1362) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f129,plain,
! [X0] :
( ~ rpoint(X0)
| ~ rR(X0,vd1361,vd1363)
| vf(vd1363,X0) != vf(vd1361,vd1362) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
rless(vf(vd1361,vd1362),vf(vd1361,vd1363)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f132,plain,
! [Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116] :
( vf(Vd1109,vskolem1120(Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116)) = vf(Vd1113,Vd1115)
| ~ rpoint(Vd1110)
| Vd1109 != Vd1110
| ~ rpoint(Vd1112)
| Vd1111 != Vd1112
| ~ rpoint(Vd1114)
| Vd1113 != Vd1114
| ~ rpoint(Vd1116)
| Vd1115 != Vd1116
| Vd1109 = Vd1111
| Vd1113 = Vd1115
| ~ rless(vf(Vd1113,Vd1115),vf(Vd1109,Vd1111)) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f133,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( vf(X2,vskolem1120(X2,X7,X3,X6,X0,X5,X1,X4)) = vf(X0,X1)
| ~ rpoint(X7)
| X2 != X7
| ~ rpoint(X6)
| X3 != X6
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| X2 = X3
| X0 = X1
| ~ rless(vf(X0,X1),vf(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f134,plain,
! [Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116] :
( rR(vskolem1120(Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116),Vd1109,Vd1111)
| ~ rpoint(Vd1110)
| Vd1109 != Vd1110
| ~ rpoint(Vd1112)
| Vd1111 != Vd1112
| ~ rpoint(Vd1114)
| Vd1113 != Vd1114
| ~ rpoint(Vd1116)
| Vd1115 != Vd1116
| Vd1109 = Vd1111
| Vd1113 = Vd1115
| ~ rless(vf(Vd1113,Vd1115),vf(Vd1109,Vd1111)) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f135,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( rR(vskolem1120(X2,X7,X3,X6,X0,X5,X1,X4),X2,X3)
| ~ rpoint(X7)
| X2 != X7
| ~ rpoint(X6)
| X3 != X6
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| X2 = X3
| X0 = X1
| ~ rless(vf(X0,X1),vf(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f136,plain,
! [Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116] :
( rpoint(vskolem1120(Vd1109,Vd1110,Vd1111,Vd1112,Vd1113,Vd1114,Vd1115,Vd1116))
| ~ rpoint(Vd1110)
| Vd1109 != Vd1110
| ~ rpoint(Vd1112)
| Vd1111 != Vd1112
| ~ rpoint(Vd1114)
| Vd1113 != Vd1114
| ~ rpoint(Vd1116)
| Vd1115 != Vd1116
| Vd1109 = Vd1111
| Vd1113 = Vd1115
| ~ rless(vf(Vd1113,Vd1115),vf(Vd1109,Vd1111)) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f137,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( rpoint(vskolem1120(X2,X7,X3,X6,X0,X5,X1,X4))
| ~ rpoint(X7)
| X2 != X7
| ~ rpoint(X6)
| X3 != X6
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| X2 = X3
| X0 = X1
| ~ rless(vf(X0,X1),vf(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f148,plain,
( rpoint(sK0_skl)
& vd1362 = sK0_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd1367,sK0_skl)],[f11]) ).
fof(f149,plain,
vd1362 = sK0_skl,
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f150,plain,
rpoint(sK0_skl),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f165,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)],[f15]) ).
fof(f166,plain,
! [X0,X1,X2,X3] :
( vf(X2,X0) = vf(X0,X2)
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f184,plain,
! [Vd340,Vd341,Vd342] :
( ( rR(Vd341,Vd342,Vd340)
& Vd340 != Vd341
& Vd340 != Vd342
& ~ rR(Vd340,Vd341,Vd342) )
| ! [Vd344] :
( ~ rpoint(Vd344)
| Vd340 != Vd344 )
| ! [Vd345] :
( ~ rpoint(Vd345)
| Vd341 != Vd345 )
| ! [Vd346] :
( ~ rpoint(Vd346)
| Vd342 != Vd346 )
| ~ rR(Vd341,Vd340,Vd342) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f188,plain,
! [X0,X1,X2,X3,X4,X5] :
( rR(X0,X2,X1)
| ~ rpoint(X5)
| X1 != X5
| ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f269,plain,
vd1361 != vd1363,
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f270,plain,
vd1361 != vd1362,
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f271,plain,
( rpoint(sK9_skl)
& vd1363 = sK9_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(Vd1368,sK9_skl)],[f46]) ).
fof(f272,plain,
vd1363 = sK9_skl,
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f273,plain,
rpoint(sK9_skl),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f274,plain,
( rpoint(sK10_skl)
& vd1361 = sK10_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(Vd1366,sK10_skl)],[f47]) ).
fof(f275,plain,
vd1361 = sK10_skl,
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f276,plain,
rpoint(sK10_skl),
inference(cnf_transformation,[status(thm)],[f274]) ).
fof(f564,plain,
! [Vd15,Vd16] :
( ? [Vd17] :
( rpoint(Vd17)
& Vd17 != Vd15 )
| ~ rpoint(Vd16)
| Vd15 != Vd16 ),
inference(pre_NNF_transformation,[status(thm)],[f110]) ).
fof(f565,plain,
! [Vd15] :
( ? [Vd17] :
( rpoint(Vd17)
& Vd17 != Vd15 )
| ! [Vd16] :
( ~ rpoint(Vd16)
| Vd15 != Vd16 ) ),
inference(miniscoping,[status(thm)],[f564]) ).
fof(f566,plain,
! [Vd15] :
( ( rpoint(sK44_skl(Vd15))
& sK44_skl(Vd15) != Vd15 )
| ! [Vd16] :
( ~ rpoint(Vd16)
| Vd15 != Vd16 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44_skl]),skolemize(Vd17,sK44_skl(Vd15))],[f565]) ).
fof(f567,plain,
! [X0,X1] :
( sK44_skl(X0) != X0
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f566]) ).
fof(f568,plain,
! [X0,X1] :
( rpoint(sK44_skl(X0))
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f566]) ).
fof(f701,plain,
! [X0,X1,X2,X3] :
( vf(X2,vskolem1120(X2,X2,X3,X3,X0,X0,X1,X1)) = vf(X0,X1)
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X1)
| X2 = X3
| X0 = X1
| ~ rless(vf(X0,X1),vf(X2,X3)) ),
inference(destructive_equality_resolution,[status(thm)],[f133]) ).
fof(f702,plain,
! [X0,X1,X2,X3] :
( rR(vskolem1120(X2,X2,X3,X3,X0,X0,X1,X1),X2,X3)
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X1)
| X2 = X3
| X0 = X1
| ~ rless(vf(X0,X1),vf(X2,X3)) ),
inference(destructive_equality_resolution,[status(thm)],[f135]) ).
fof(f703,plain,
! [X0,X1,X2,X3] :
( rpoint(vskolem1120(X2,X2,X3,X3,X0,X0,X1,X1))
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rpoint(X1)
| X2 = X3
| X0 = X1
| ~ rless(vf(X0,X1),vf(X2,X3)) ),
inference(destructive_equality_resolution,[status(thm)],[f137]) ).
fof(f715,plain,
! [X0,X1] :
( vf(X1,X0) = vf(X0,X1)
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f166]) ).
fof(f729,plain,
! [X0,X1,X2] :
( rR(X0,X2,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rR(X0,X1,X2) ),
inference(destructive_equality_resolution,[status(thm)],[f188]) ).
fof(f899,plain,
! [X0] :
( sK44_skl(X0) != X0
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f567]) ).
fof(f900,plain,
! [X0] :
( rpoint(sK44_skl(X0))
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f568]) ).
fof(f939,plain,
rless(vf(vd1361,sK0_skl),vf(vd1361,vd1363)),
inference(backward_demodulation,[status(thm)],[f149,f130]) ).
fof(f940,plain,
! [X0] :
( ~ rpoint(X0)
| ~ rR(X0,vd1361,vd1363)
| vf(vd1363,X0) != vf(vd1361,sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f149,f129]) ).
fof(f941,plain,
vd1361 != sK0_skl,
inference(forward_demodulation,[status(thm)],[f149,f270]) ).
fof(f942,plain,
! [X0] :
( vf(X0,sK0_skl) = vf(sK0_skl,X0)
| ~ rpoint(X0) ),
inference(resolution,[status(thm)],[f150,f715]) ).
fof(f948,plain,
! [X0] :
( ~ rpoint(X0)
| ~ rR(X0,vd1361,sK9_skl)
| vf(vd1363,X0) != vf(vd1361,sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f272,f940]) ).
fof(f949,plain,
vd1361 != sK9_skl,
inference(backward_demodulation,[status(thm)],[f272,f269]) ).
fof(f950,plain,
! [X0] :
( ~ rpoint(X0)
| ~ rR(X0,vd1361,sK9_skl)
| vf(sK9_skl,X0) != vf(vd1361,sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f272,f948]) ).
fof(f951,plain,
! [X0] :
( vf(X0,sK9_skl) = vf(sK9_skl,X0)
| ~ rpoint(X0) ),
inference(resolution,[status(thm)],[f273,f715]) ).
fof(f952,plain,
sK10_skl != sK0_skl,
inference(backward_demodulation,[status(thm)],[f275,f941]) ).
fof(f953,plain,
! [X0] :
( ~ rpoint(X0)
| ~ rR(X0,vd1361,sK9_skl)
| vf(sK9_skl,X0) != vf(sK10_skl,sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f275,f950]) ).
fof(f954,plain,
! [X0] :
( ~ rpoint(X0)
| ~ rR(X0,sK10_skl,sK9_skl)
| vf(sK9_skl,X0) != vf(sK10_skl,sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f275,f953]) ).
fof(f955,plain,
sK10_skl != sK9_skl,
inference(forward_demodulation,[status(thm)],[f275,f949]) ).
fof(f967,plain,
vf(sK10_skl,sK0_skl) = vf(sK0_skl,sK10_skl),
inference(resolution,[status(thm)],[f942,f276]) ).
fof(f982,definition,
( sQ10_spl
<=> rpoint(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f984,plain,
( sQ10_spl
| ~ rpoint(sK0_skl) ),
inference(component_clause,[status(thm)],[f982]) ).
fof(f1011,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f984,f150]) ).
fof(f1012,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f1011]) ).
fof(f1015,plain,
sK44_skl(sK10_skl) != sK10_skl,
inference(resolution,[status(thm)],[f899,f276]) ).
fof(f1023,plain,
! [X0] :
( ~ rpoint(X0)
| ~ rR(X0,sK10_skl,sK9_skl)
| vf(sK9_skl,X0) != vf(sK0_skl,sK10_skl) ),
inference(backward_demodulation,[status(thm)],[f967,f954]) ).
fof(f1033,definition,
( sQ18_spl
<=> sK10_skl = sK0_skl ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1034,plain,
( ~ sQ18_spl
| sK10_skl = sK0_skl ),
inference(component_clause,[status(thm)],[f1033]) ).
fof(f1036,definition,
( sQ19_spl
<=> rpoint(sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f1038,plain,
( sQ19_spl
| ~ rpoint(sK10_skl) ),
inference(component_clause,[status(thm)],[f1036]) ).
fof(f1060,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1038,f276]) ).
fof(f1061,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f1060]) ).
fof(f1062,plain,
( ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1034,f952]) ).
fof(f1063,plain,
~ sQ18_spl,
inference(contradiction_clause,[status(thm)],[f1062]) ).
fof(f1077,definition,
( sQ27_spl
<=> rpoint(sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1079,plain,
( sQ27_spl
| ~ rpoint(sK9_skl) ),
inference(component_clause,[status(thm)],[f1077]) ).
fof(f1101,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1079,f273]) ).
fof(f1102,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f1101]) ).
fof(f1114,plain,
vf(sK10_skl,sK9_skl) = vf(sK9_skl,sK10_skl),
inference(resolution,[status(thm)],[f951,f276]) ).
fof(f1117,plain,
rless(vf(sK10_skl,sK0_skl),vf(vd1361,vd1363)),
inference(forward_demodulation,[status(thm)],[f275,f939]) ).
fof(f1118,plain,
rless(vf(sK0_skl,sK10_skl),vf(vd1361,vd1363)),
inference(forward_demodulation,[status(thm)],[f967,f1117]) ).
fof(f1119,plain,
rless(vf(sK0_skl,sK10_skl),vf(sK10_skl,vd1363)),
inference(forward_demodulation,[status(thm)],[f275,f1118]) ).
fof(f1120,plain,
rless(vf(sK0_skl,sK10_skl),vf(sK10_skl,sK9_skl)),
inference(forward_demodulation,[status(thm)],[f272,f1119]) ).
fof(f1124,definition,
( sQ33_spl
<=> sK10_skl = sK9_skl ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1125,plain,
( ~ sQ33_spl
| sK10_skl = sK9_skl ),
inference(component_clause,[status(thm)],[f1124]) ).
fof(f1139,plain,
( ~ sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1125,f955]) ).
fof(f1140,plain,
~ sQ33_spl,
inference(contradiction_clause,[status(thm)],[f1139]) ).
fof(f1141,plain,
rless(vf(sK0_skl,sK10_skl),vf(sK9_skl,sK10_skl)),
inference(backward_demodulation,[status(thm)],[f1114,f1120]) ).
fof(f1175,plain,
( rpoint(vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl))
| ~ rpoint(sK9_skl)
| ~ rpoint(sK10_skl)
| ~ rpoint(sK0_skl)
| ~ rpoint(sK10_skl)
| sK9_skl = sK10_skl
| sK0_skl = sK10_skl ),
inference(resolution,[status(thm)],[f1141,f703]) ).
fof(f1176,plain,
( rR(vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl),sK9_skl,sK10_skl)
| ~ rpoint(sK9_skl)
| ~ rpoint(sK10_skl)
| ~ rpoint(sK0_skl)
| ~ rpoint(sK10_skl)
| sK9_skl = sK10_skl
| sK0_skl = sK10_skl ),
inference(resolution,[status(thm)],[f1141,f702]) ).
fof(f1177,plain,
( vf(sK9_skl,vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl)) = vf(sK0_skl,sK10_skl)
| ~ rpoint(sK9_skl)
| ~ rpoint(sK10_skl)
| ~ rpoint(sK0_skl)
| ~ rpoint(sK10_skl)
| sK9_skl = sK10_skl
| sK0_skl = sK10_skl ),
inference(resolution,[status(thm)],[f1141,f701]) ).
fof(f1178,definition,
( sQ43_spl
<=> rpoint(vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1181,plain,
( sQ43_spl
| ~ sQ27_spl
| ~ sQ10_spl
| ~ sQ19_spl
| sQ33_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1175,f1033,f1124,f1036,f982,f1077,f1178]) ).
fof(f1182,definition,
( sQ44_spl
<=> rR(vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl),sK9_skl,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1183,plain,
( ~ sQ44_spl
| rR(vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl),sK9_skl,sK10_skl) ),
inference(component_clause,[status(thm)],[f1182]) ).
fof(f1185,plain,
( sQ44_spl
| ~ sQ27_spl
| ~ sQ10_spl
| ~ sQ19_spl
| sQ33_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1176,f1033,f1124,f1036,f982,f1077,f1182]) ).
fof(f1186,definition,
( sQ45_spl
<=> vf(sK9_skl,vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl)) = vf(sK0_skl,sK10_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f1189,plain,
( sQ45_spl
| ~ sQ27_spl
| ~ sQ10_spl
| ~ sQ19_spl
| sQ33_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f1177,f1033,f1124,f1036,f982,f1077,f1186]) ).
fof(f1286,plain,
( ~ sQ44_spl
| rR(vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl),sK10_skl,sK9_skl)
| ~ rpoint(sK9_skl)
| ~ rpoint(vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl))
| ~ rpoint(sK10_skl) ),
inference(resolution,[status(thm)],[f1183,f729]) ).
fof(f1308,definition,
( sQ66_spl
<=> rR(vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl),sK10_skl,sK9_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1309,plain,
( ~ sQ66_spl
| rR(vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl),sK10_skl,sK9_skl) ),
inference(component_clause,[status(thm)],[f1308]) ).
fof(f1311,plain,
( ~ sQ44_spl
| sQ66_spl
| ~ sQ27_spl
| ~ sQ43_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f1286,f1036,f1178,f1077,f1308,f1182]) ).
fof(f1412,plain,
rpoint(sK44_skl(sK10_skl)),
inference(resolution,[status(thm)],[f900,f276]) ).
fof(f1413,plain,
rpoint(sK44_skl(sK9_skl)),
inference(resolution,[status(thm)],[f900,f273]) ).
fof(f1528,definition,
( sQ93_spl
<=> sK44_skl(sK10_skl) = sK10_skl ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f1529,plain,
( ~ sQ93_spl
| sK44_skl(sK10_skl) = sK10_skl ),
inference(component_clause,[status(thm)],[f1528]) ).
fof(f1531,definition,
( sQ94_spl
<=> rpoint(sK44_skl(sK10_skl)) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1533,plain,
( sQ94_spl
| ~ rpoint(sK44_skl(sK10_skl)) ),
inference(component_clause,[status(thm)],[f1531]) ).
fof(f1555,plain,
( sQ94_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1533,f1412]) ).
fof(f1556,plain,
sQ94_spl,
inference(contradiction_clause,[status(thm)],[f1555]) ).
fof(f1557,plain,
( ~ sQ93_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1529,f1015]) ).
fof(f1558,plain,
~ sQ93_spl,
inference(contradiction_clause,[status(thm)],[f1557]) ).
fof(f1714,definition,
( sQ122_spl
<=> rpoint(sK44_skl(sK9_skl)) ),
introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition]) ).
fof(f1716,plain,
( sQ122_spl
| ~ rpoint(sK44_skl(sK9_skl)) ),
inference(component_clause,[status(thm)],[f1714]) ).
fof(f1738,plain,
( sQ122_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1716,f1413]) ).
fof(f1739,plain,
sQ122_spl,
inference(contradiction_clause,[status(thm)],[f1738]) ).
fof(f2239,plain,
( ~ sQ66_spl
| ~ rpoint(vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl))
| vf(sK9_skl,vskolem1120(sK9_skl,sK9_skl,sK10_skl,sK10_skl,sK0_skl,sK0_skl,sK10_skl,sK10_skl)) != vf(sK0_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f1309,f1023]) ).
fof(f2247,plain,
( ~ sQ66_spl
| ~ sQ43_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f2239,f1186,f1178,f1308]) ).
fof(f2273,plain,
$false,
inference(sat_refutation,[status(thm)],[f1012,f1061,f1063,f1102,f1140,f1181,f1185,f1189,f1311,f1556,f1558,f1739,f2247]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO336+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n003.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:31:15 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.40 % Drodi V4.1.1
% 3.27/0.90 % Refutation found
% 3.27/0.90 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.27/0.90 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.51/0.92 % Elapsed time: 0.528760 seconds
% 0.51/0.92 % CPU time: 3.811991 seconds
% 0.51/0.92 % Total memory used: 147.642 MB
% 0.51/0.92 % Net memory used: 143.438 MB
%------------------------------------------------------------------------------