%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO497+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:25:07 PM UTC 2026
% Result : Theorem 134.09s 22.51s
% Output : CNFRefutation 134.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 25
% Syntax : Number of formulae : 104 ( 20 unt; 13 def)
% Number of atoms : 277 ( 64 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 311 ( 138 ~; 134 |; 26 &)
% ( 13 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 13 prp; 0-4 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-4 aty)
% Number of variables : 236 ( 220 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X,Y,Z] :
( X = Y
| ~ s_e(X,Y,Z,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y,W,V] :
( s_e(Y,ext(X,Y,W,V),W,V)
& s_t(X,Y,ext(X,Y,W,V)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [Xa,Xb] : s_e(Xa,Xa,Xb,Xb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [Xa,Xb,Xc] :
( s_t(Xc,Xb,Xa)
| ~ s_t(Xa,Xb,Xc) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [Xb,Xa] : Xb != ext(Xa,Xb,alpha,gamma),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [Xa,Xb,Xc,Xd,Xa1,Xb1,Xc1,Xd1] :
( le(Xa1,Xb1,Xc1,Xd1)
| ~ s_e(Xc,Xd,Xc1,Xd1)
| ~ s_e(Xa,Xb,Xa1,Xb1)
| ~ le(Xa,Xb,Xc,Xd) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [Xa,Xb,Xc,Xd,Xe,Xf] :
( le(Xa,Xb,Xe,Xf)
| ~ le(Xc,Xd,Xe,Xf)
| ~ le(Xa,Xb,Xc,Xd) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [Xa,Xc,Xd] : le(Xa,Xa,Xc,Xd),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [Xa,Xp,Xb,Xc] :
( sameside(Xa,Xp,Xb)
| ~ s_t(Xb,Xp,Xc)
| ~ s_t(Xa,Xp,Xc)
| Xc = Xp
| Xb = Xp
| Xa = Xp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,conjecture,
! [Xr,Xa,Xb,Xc] :
( ( s_e(Xa,insert(Xb,Xc,Xa,Xr),Xb,Xc)
| Xb = Xc
| Xr = Xa )
& ( sameside(insert(Xb,Xc,Xa,Xr),Xa,Xr)
| Xb = Xc
| Xr = Xa ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,negated_conjecture,
~ ! [Xr,Xa,Xb,Xc] :
( ( s_e(Xa,insert(Xb,Xc,Xa,Xr),Xb,Xc)
| Xb = Xc
| Xr = Xa )
& ( sameside(insert(Xb,Xc,Xa,Xr),Xa,Xr)
| Xb = Xc
| Xr = Xa ) ),
inference(negated_conjecture,[status(cth)],[f77]) ).
fof(f79,axiom,
! [Xa,Xb,Xa1,Xc1] : insert(Xa,Xb,Xa1,Xc1) = ext(ext(Xc1,Xa1,alpha,gamma),Xa1,Xa,Xb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [Xa,Xb,Xc,Xd,Y] :
( ( le(Xa,Xb,Xc,Xd)
| ~ s_e(Xa,Xb,Xc,Y)
| ~ s_t(Xc,Y,Xd) )
& ( s_e(Xa,Xb,Xc,insert(Xa,Xb,Xc,Xd))
| ~ le(Xa,Xb,Xc,Xd) )
& ( s_t(Xc,insert(Xa,Xb,Xc,Xd),Xd)
| ~ le(Xa,Xb,Xc,Xd) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f90,plain,
! [X,Y] :
( X = Y
| ! [Z] : ~ s_e(X,Y,Z,Z) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f91,plain,
! [X0,X1,X2] :
( X0 = X1
| ~ s_e(X0,X1,X2,X2) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f92,plain,
( ! [X,Y,W,V] : s_e(Y,ext(X,Y,W,V),W,V)
& ! [X,Y,W,V] : s_t(X,Y,ext(X,Y,W,V)) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f93,plain,
! [X0,X1,X2,X3] : s_t(X0,X1,ext(X0,X1,X2,X3)),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f94,plain,
! [X0,X1,X2,X3] : s_e(X0,ext(X1,X0,X2,X3),X2,X3),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f110,plain,
! [X0,X1] : s_e(X0,X0,X1,X1),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f120,plain,
! [X0,X1,X2] :
( s_t(X2,X1,X0)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f140,plain,
! [X0,X1] : X0 != ext(X1,X0,alpha,gamma),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f183,plain,
! [Xa1,Xb1,Xc1,Xd1] :
( le(Xa1,Xb1,Xc1,Xd1)
| ! [Xc,Xd] :
( ~ s_e(Xc,Xd,Xc1,Xd1)
| ! [Xa,Xb] :
( ~ s_e(Xa,Xb,Xa1,Xb1)
| ~ le(Xa,Xb,Xc,Xd) ) ) ),
inference(miniscoping,[status(thm)],[f58]) ).
fof(f184,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( le(X4,X5,X6,X7)
| ~ s_e(X2,X3,X6,X7)
| ~ s_e(X0,X1,X4,X5)
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f186,plain,
! [Xa,Xb,Xe,Xf] :
( le(Xa,Xb,Xe,Xf)
| ! [Xc,Xd] :
( ~ le(Xc,Xd,Xe,Xf)
| ~ le(Xa,Xb,Xc,Xd) ) ),
inference(miniscoping,[status(thm)],[f60]) ).
fof(f187,plain,
! [X0,X1,X2,X3,X4,X5] :
( le(X0,X1,X4,X5)
| ~ le(X2,X3,X4,X5)
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f190,plain,
! [X0,X1,X2] : le(X0,X0,X1,X2),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f196,plain,
! [Xa,Xp,Xb] :
( sameside(Xa,Xp,Xb)
| ! [Xc] :
( ~ s_t(Xb,Xp,Xc)
| ~ s_t(Xa,Xp,Xc)
| Xc = Xp
| Xb = Xp
| Xa = Xp ) ),
inference(miniscoping,[status(thm)],[f68]) ).
fof(f197,plain,
! [X0,X1,X2,X3] :
( sameside(X0,X1,X2)
| ~ s_t(X2,X1,X3)
| ~ s_t(X0,X1,X3)
| X3 = X1
| X2 = X1
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f196]) ).
fof(f216,plain,
? [Xr,Xa,Xb,Xc] :
( ( ~ s_e(Xa,insert(Xb,Xc,Xa,Xr),Xb,Xc)
& Xb != Xc
& Xr != Xa )
| ( ~ sameside(insert(Xb,Xc,Xa,Xr),Xa,Xr)
& Xb != Xc
& Xr != Xa ) ),
inference(pre_NNF_transformation,[status(thm)],[f78]) ).
fof(f217,definition,
! [Xr,Xa,Xb,Xc] :
( sP0_prd(Xc,Xb,Xa,Xr)
<=> ( ~ sameside(insert(Xb,Xc,Xa,Xr),Xa,Xr)
& Xb != Xc
& Xr != Xa ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f218,plain,
? [Xr,Xa,Xb,Xc] :
( ( ~ s_e(Xa,insert(Xb,Xc,Xa,Xr),Xb,Xc)
& Xb != Xc
& Xr != Xa )
| sP0_prd(Xc,Xb,Xa,Xr) ),
inference(formula_renaming,[status(thm)],[f216,f217]) ).
fof(f219,plain,
( ? [Xr,Xa,Xb,Xc] :
( ~ s_e(Xa,insert(Xb,Xc,Xa,Xr),Xb,Xc)
& Xb != Xc
& Xr != Xa )
| ? [Xr,Xa,Xb,Xc] : sP0_prd(Xc,Xb,Xa,Xr) ),
inference(miniscoping,[status(thm)],[f218]) ).
fof(f220,plain,
( ( ~ s_e(sK5_skl,insert(sK6_skl,sK7_skl,sK5_skl,sK4_skl),sK6_skl,sK7_skl)
& sK6_skl != sK7_skl
& sK4_skl != sK5_skl )
| sP0_prd(sK3_skl,sK2_skl,sK1_skl,sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl]),skolemize(Xr,sK0_skl),skolemize(Xa,sK1_skl),skolemize(Xb,sK2_skl),skolemize(Xc,sK3_skl),skolemize(Xr,sK4_skl),skolemize(Xa,sK5_skl),skolemize(Xb,sK6_skl),skolemize(Xc,sK7_skl)],[f219]) ).
fof(f223,plain,
( ~ s_e(sK5_skl,insert(sK6_skl,sK7_skl,sK5_skl,sK4_skl),sK6_skl,sK7_skl)
| sP0_prd(sK3_skl,sK2_skl,sK1_skl,sK0_skl) ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f224,plain,
! [X0,X1,X2,X3] : insert(X0,X1,X2,X3) = ext(ext(X3,X2,alpha,gamma),X2,X0,X1),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f257,plain,
( ! [Xa,Xb,Xc,Xd] :
( le(Xa,Xb,Xc,Xd)
| ! [Y] :
( ~ s_e(Xa,Xb,Xc,Y)
| ~ s_t(Xc,Y,Xd) ) )
& ! [Xa,Xb,Xc,Xd] :
( s_e(Xa,Xb,Xc,insert(Xa,Xb,Xc,Xd))
| ~ le(Xa,Xb,Xc,Xd) )
& ! [Xa,Xb,Xc,Xd] :
( s_t(Xc,insert(Xa,Xb,Xc,Xd),Xd)
| ~ le(Xa,Xb,Xc,Xd) ) ),
inference(miniscoping,[status(thm)],[f85]) ).
fof(f259,plain,
! [X0,X1,X2,X3] :
( s_e(X0,X1,X2,insert(X0,X1,X2,X3))
| ~ le(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f257]) ).
fof(f267,plain,
! [Xr,Xa,Xb,Xc] :
( ( sameside(insert(Xb,Xc,Xa,Xr),Xa,Xr)
| Xb = Xc
| Xr = Xa
| sP0_prd(Xc,Xb,Xa,Xr) )
& ( ( ~ sameside(insert(Xb,Xc,Xa,Xr),Xa,Xr)
& Xb != Xc
& Xr != Xa )
| ~ sP0_prd(Xc,Xb,Xa,Xr) ) ),
inference(NNF_transformation,[status(thm)],[f217]) ).
fof(f268,plain,
( ! [Xr,Xa,Xb,Xc] :
( sameside(insert(Xb,Xc,Xa,Xr),Xa,Xr)
| Xb = Xc
| Xr = Xa
| sP0_prd(Xc,Xb,Xa,Xr) )
& ! [Xr,Xa,Xb,Xc] :
( ( ~ sameside(insert(Xb,Xc,Xa,Xr),Xa,Xr)
& Xb != Xc
& Xr != Xa )
| ~ sP0_prd(Xc,Xb,Xa,Xr) ) ),
inference(miniscoping,[status(thm)],[f267]) ).
fof(f269,plain,
! [X0,X1,X2,X3] :
( X3 != X2
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f270,plain,
! [X0,X1,X2,X3] :
( X1 != X0
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f271,plain,
! [X0,X1,X2,X3] :
( ~ sameside(insert(X1,X0,X2,X3),X2,X3)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f273,definition,
( sQ0_spl
<=> sP0_prd(sK3_skl,sK2_skl,sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f274,plain,
( ~ sQ0_spl
| sP0_prd(sK3_skl,sK2_skl,sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f273]) ).
fof(f284,definition,
( sQ3_spl
<=> s_e(sK5_skl,insert(sK6_skl,sK7_skl,sK5_skl,sK4_skl),sK6_skl,sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f286,plain,
( sQ3_spl
| ~ s_e(sK5_skl,insert(sK6_skl,sK7_skl,sK5_skl,sK4_skl),sK6_skl,sK7_skl) ),
inference(component_clause,[status(thm)],[f284]) ).
fof(f287,plain,
( ~ sQ3_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f223,f273,f284]) ).
fof(f292,plain,
! [X0,X1,X2] : ~ sP0_prd(X0,X1,X2,X2),
inference(destructive_equality_resolution,[status(thm)],[f269]) ).
fof(f293,plain,
! [X0,X1,X2] : ~ sP0_prd(X0,X0,X1,X2),
inference(destructive_equality_resolution,[status(thm)],[f270]) ).
fof(f347,plain,
! [X0,X1,X2,X3] : s_t(ext(X0,X1,X2,X3),X1,X0),
inference(resolution,[status(thm)],[f120,f93]) ).
fof(f371,plain,
! [X0,X1,X2,X3,X4] :
( ~ sP0_prd(X1,X0,X2,X3)
| ~ s_t(X3,X2,X4)
| ~ s_t(insert(X0,X1,X2,X3),X2,X4)
| X4 = X2
| X3 = X2
| insert(X0,X1,X2,X3) = X2 ),
inference(resolution,[status(thm)],[f197,f271]) ).
fof(f416,plain,
! [X0] :
( ~ sQ0_spl
| ~ s_t(sK0_skl,sK1_skl,X0)
| ~ s_t(insert(sK2_skl,sK3_skl,sK1_skl,sK0_skl),sK1_skl,X0)
| X0 = sK1_skl
| sK0_skl = sK1_skl
| insert(sK2_skl,sK3_skl,sK1_skl,sK0_skl) = sK1_skl ),
inference(resolution,[status(thm)],[f371,f274]) ).
fof(f417,definition,
( sQ4_spl
<=> insert(sK2_skl,sK3_skl,sK1_skl,sK0_skl) = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f418,plain,
( ~ sQ4_spl
| insert(sK2_skl,sK3_skl,sK1_skl,sK0_skl) = sK1_skl ),
inference(component_clause,[status(thm)],[f417]) ).
fof(f420,definition,
( sQ5_spl
<=> sK0_skl = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f421,plain,
( ~ sQ5_spl
| sK0_skl = sK1_skl ),
inference(component_clause,[status(thm)],[f420]) ).
fof(f423,definition,
! [X0] :
( sQ6_spl
<=> ( ~ s_t(sK0_skl,sK1_skl,X0)
| ~ s_t(insert(sK2_skl,sK3_skl,sK1_skl,sK0_skl),sK1_skl,X0)
| X0 = sK1_skl ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f424,plain,
! [X0] :
( ~ sQ6_spl
| ~ s_t(sK0_skl,sK1_skl,X0)
| ~ s_t(insert(sK2_skl,sK3_skl,sK1_skl,sK0_skl),sK1_skl,X0)
| X0 = sK1_skl ),
inference(component_clause,[status(thm)],[f423]) ).
fof(f426,plain,
( ~ sQ0_spl
| sQ6_spl
| sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f416,f417,f420,f423,f273]) ).
fof(f611,plain,
( ~ sQ0_spl
| ~ sQ5_spl
| sP0_prd(sK3_skl,sK2_skl,sK0_skl,sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f421,f274]) ).
fof(f612,plain,
( ~ sQ0_spl
| ~ sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f611,f292]) ).
fof(f613,plain,
( ~ sQ0_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f612]) ).
fof(f630,definition,
( sQ10_spl
<=> sK2_skl = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f631,plain,
( ~ sQ10_spl
| sK2_skl = sK3_skl ),
inference(component_clause,[status(thm)],[f630]) ).
fof(f690,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( le(X1,X2,X5,X6)
| ~ s_e(X3,X4,X5,X6)
| ~ s_e(X0,X0,X1,X2) ),
inference(resolution,[status(thm)],[f184,f190]) ).
fof(f693,plain,
! [X0,X1,X2,X3,X4] :
( le(X0,X1,X3,X4)
| ~ le(X0,X1,X2,X2) ),
inference(resolution,[status(thm)],[f187,f190]) ).
fof(f707,plain,
( ~ sQ4_spl
| s_e(sK2_skl,sK3_skl,sK1_skl,sK1_skl)
| ~ le(sK2_skl,sK3_skl,sK1_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f418,f259]) ).
fof(f720,definition,
( sQ17_spl
<=> le(sK2_skl,sK3_skl,sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f722,plain,
( sQ17_spl
| ~ le(sK2_skl,sK3_skl,sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f720]) ).
fof(f723,definition,
( sQ18_spl
<=> s_e(sK2_skl,sK3_skl,sK1_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f724,plain,
( ~ sQ18_spl
| s_e(sK2_skl,sK3_skl,sK1_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f723]) ).
fof(f726,plain,
( ~ sQ4_spl
| sQ18_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f707,f720,f723,f417]) ).
fof(f1079,plain,
! [X0,X1,X2,X3] : s_t(insert(X0,X1,X2,X3),X2,ext(X3,X2,alpha,gamma)),
inference(paramodulation,[status(thm)],[f224,f347]) ).
fof(f1081,plain,
! [X0,X1,X2,X3] : s_e(X0,insert(X1,X2,X0,X3),X1,X2),
inference(paramodulation,[status(thm)],[f224,f94]) ).
fof(f3276,plain,
( ~ sQ18_spl
| sK2_skl = sK3_skl ),
inference(resolution,[status(thm)],[f724,f91]) ).
fof(f3277,plain,
( ~ sQ18_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f3276,f630,f723]) ).
fof(f3290,plain,
( ~ sQ0_spl
| ~ sQ10_spl
| sP0_prd(sK2_skl,sK2_skl,sK1_skl,sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f631,f274]) ).
fof(f3293,plain,
( ~ sQ0_spl
| ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3290,f293]) ).
fof(f3294,plain,
( ~ sQ0_spl
| ~ sQ10_spl ),
inference(contradiction_clause,[status(thm)],[f3293]) ).
fof(f3556,definition,
! [X1,X2,X3] :
( sQ64_spl
<=> ~ s_e(X1,X2,X3,X3) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f3557,plain,
! [X0,X1,X2] :
( ~ sQ64_spl
| ~ s_e(X0,X1,X2,X2) ),
inference(component_clause,[status(thm)],[f3556]) ).
fof(f3715,plain,
( ~ sQ64_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f110,f3557]) ).
fof(f3730,plain,
~ sQ64_spl,
inference(contradiction_clause,[status(thm)],[f3715]) ).
fof(f4277,plain,
! [X0] :
( sQ17_spl
| ~ le(sK2_skl,sK3_skl,X0,X0) ),
inference(resolution,[status(thm)],[f722,f693]) ).
fof(f4286,definition,
! [X0] :
( sQ69_spl
<=> ~ s_e(X0,X0,sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f4287,plain,
! [X0] :
( ~ sQ69_spl
| ~ s_e(X0,X0,sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f4286]) ).
fof(f4322,plain,
! [X0,X1,X2,X3] :
( sQ17_spl
| ~ s_e(X1,X2,X3,X3)
| ~ s_e(X0,X0,sK2_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f4277,f690]) ).
fof(f4341,plain,
( sQ17_spl
| sQ64_spl
| sQ69_spl ),
inference(split_clause,[status(thm)],[f4322,f4286,f3556,f720]) ).
fof(f6514,plain,
( ~ sQ4_spl
| s_e(sK1_skl,sK1_skl,sK2_skl,sK3_skl) ),
inference(paramodulation,[status(thm)],[f418,f1081]) ).
fof(f6529,plain,
( ~ sQ4_spl
| ~ sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6514,f4287]) ).
fof(f6530,plain,
( ~ sQ4_spl
| ~ sQ69_spl ),
inference(contradiction_clause,[status(thm)],[f6529]) ).
fof(f6544,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f286,f1081]) ).
fof(f6545,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f6544]) ).
fof(f9048,plain,
( ~ sQ6_spl
| ~ s_t(sK0_skl,sK1_skl,ext(sK0_skl,sK1_skl,alpha,gamma))
| ext(sK0_skl,sK1_skl,alpha,gamma) = sK1_skl ),
inference(resolution,[status(thm)],[f1079,f424]) ).
fof(f9147,definition,
( sQ152_spl
<=> ext(sK0_skl,sK1_skl,alpha,gamma) = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition]) ).
fof(f9148,plain,
( ~ sQ152_spl
| ext(sK0_skl,sK1_skl,alpha,gamma) = sK1_skl ),
inference(component_clause,[status(thm)],[f9147]) ).
fof(f9150,definition,
( sQ153_spl
<=> s_t(sK0_skl,sK1_skl,ext(sK0_skl,sK1_skl,alpha,gamma)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f9152,plain,
( sQ153_spl
| ~ s_t(sK0_skl,sK1_skl,ext(sK0_skl,sK1_skl,alpha,gamma)) ),
inference(component_clause,[status(thm)],[f9150]) ).
fof(f9153,plain,
( ~ sQ6_spl
| ~ sQ153_spl
| sQ152_spl ),
inference(split_clause,[status(thm)],[f9048,f9147,f9150,f423]) ).
fof(f9176,plain,
( ~ sQ152_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9148,f140]) ).
fof(f9177,plain,
~ sQ152_spl,
inference(contradiction_clause,[status(thm)],[f9176]) ).
fof(f9178,plain,
( sQ153_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9152,f93]) ).
fof(f9179,plain,
sQ153_spl,
inference(contradiction_clause,[status(thm)],[f9178]) ).
fof(f9180,plain,
$false,
inference(sat_refutation,[status(thm)],[f287,f426,f613,f726,f3277,f3294,f3730,f4341,f6530,f6545,f9153,f9177,f9179]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO497+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.37 % Computer : n002.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Sun Sep 20 16:57:25 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.39 % Drodi V4.1.1
% 134.09/22.51 % Refutation found
% 134.09/22.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 134.09/22.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 29.78/22.55 % Elapsed time: 17.157231 seconds
% 29.78/22.55 % CPU time: 135.895394 seconds
% 29.78/22.55 % Total memory used: 279.265 MB
% 29.78/22.55 % Net memory used: 230.630 MB
%------------------------------------------------------------------------------