%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO528+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 : n018.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:10 PM UTC 2026
% Result : Theorem 53.79s 7.47s
% Output : CNFRefutation 53.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 44
% Syntax : Number of formulae : 165 ( 46 unt; 25 def)
% Number of atoms : 360 ( 73 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 346 ( 151 ~; 148 |; 22 &)
% ( 25 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 26 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-4 aty)
% Number of variables : 142 ( 138 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
( ~ s_t(gamma,alpha,beta)
& ~ s_t(beta,gamma,alpha)
& ~ s_t(alpha,beta,gamma) ),
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(f30,axiom,
alpha != beta,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
beta != gamma,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
alpha != gamma,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [Xa,Xb,Xc] :
( s_col(Xb,Xc,Xa)
| ~ s_col(Xa,Xb,Xc) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [Xa,Xb,Xc] :
( s_col(Xc,Xa,Xb)
| ~ s_col(Xa,Xb,Xc) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [Xa,Xb,Xc] :
( s_col(Xc,Xb,Xa)
| ~ s_col(Xa,Xb,Xc) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [Xa,Xb] : s_col(Xa,Xa,Xb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [Xa,Xb] : s_col(Xa,Xb,Xa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [Xp,Xq,Xr] :
( s_col(Xq,Xp,Xr)
| ~ s_col(Xp,Xq,Xr)
| Xp = Xq ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f146,axiom,
! [Xa,Xb] : s_m(Xa,midpoint(Xa,Xb),Xb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f184,axiom,
! [Xa,Xb,Xp] :
( ( perp(Xa,Xb,Xp,reflect(Xa,Xb,Xp))
| Xp = reflect(Xa,Xb,Xp)
| Xa = Xb )
& ( s_col(Xa,Xb,midpoint(Xp,reflect(Xa,Xb,Xp)))
| Xa = Xb ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f186,axiom,
! [Xa,Xb,Xp,Xp1] :
( reflect(Xa,Xb,Xp1) = Xp
| reflect(Xa,Xb,Xp) != Xp1
| Xa = Xb ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,axiom,
! [Xa,Xb,Xp] :
( s_col(Xa,Xb,Xp)
| reflect(Xa,Xb,Xp) != Xp
| Xa = Xb ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,axiom,
! [Xa,Xb,Xp] :
( reflect(Xa,Xb,Xp) = Xp
| ~ s_col(Xa,Xb,Xp)
| Xa = Xb ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f198,conjecture,
! [Xa,Xb,Xp,Xp1] :
( opposite(Xp,Xa,Xb,Xp1)
| s_col(Xa,Xb,Xp)
| reflect(Xa,Xb,Xp) != Xp1
| Xa = Xb ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,negated_conjecture,
~ ! [Xa,Xb,Xp,Xp1] :
( opposite(Xp,Xa,Xb,Xp1)
| s_col(Xa,Xb,Xp)
| reflect(Xa,Xb,Xp) != Xp1
| Xa = Xb ),
inference(negated_conjecture,[status(cth)],[f198]) ).
fof(f208,axiom,
! [Xa,Xm,Xb] :
( ( s_m(Xa,Xm,Xb)
| ~ s_e(Xm,Xa,Xm,Xb)
| ~ s_t(Xa,Xm,Xb) )
& ( s_e(Xm,Xa,Xm,Xb)
| ~ s_m(Xa,Xm,Xb) )
& ( s_t(Xa,Xm,Xb)
| ~ s_m(Xa,Xm,Xb) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f213,axiom,
! [Xp,Xq,Xa,Xb,Xt] :
( ( s_col(Xp,Xq,il(Xa,Xb,Xp,Xq))
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( s_t(Xa,il(Xa,Xb,Xp,Xq),Xb)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( ~ s_col(Xp,Xq,Xb)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( ~ s_col(Xp,Xq,Xa)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( opposite(Xa,Xp,Xq,Xb)
| ~ s_col(Xp,Xq,Xt)
| ~ s_t(Xa,Xt,Xb)
| s_col(Xp,Xq,Xb)
| s_col(Xp,Xq,Xa)
| Xp = Xq ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f229,plain,
~ s_t(alpha,beta,gamma),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f230,plain,
~ s_t(beta,gamma,alpha),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f231,plain,
~ s_t(gamma,alpha,beta),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f248,plain,
! [X0,X1,X2] :
( ~ s_t(X2,X1,X0)
| s_t(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f264,plain,
beta != alpha,
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f265,plain,
gamma != beta,
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f266,plain,
alpha != gamma,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f281,plain,
! [X0,X1,X2] :
( s_col(X1,X2,X0)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f282,plain,
! [X0,X1,X2] :
( s_col(X2,X0,X1)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f283,plain,
! [X0,X1,X2] :
( s_col(X2,X1,X0)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f286,plain,
! [X0,X1] : s_col(X0,X0,X1),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f287,plain,
! [X0,X1] : s_col(X0,X1,X0),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f364,plain,
! [X0,X1,X2] :
( X1 = X0
| ~ s_col(X1,X0,X2)
| s_col(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f470,plain,
! [X0,X1] : s_m(X0,midpoint(X0,X1),X1),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f538,plain,
( ! [Xa,Xb,Xp] :
( perp(Xa,Xb,Xp,reflect(Xa,Xb,Xp))
| Xp = reflect(Xa,Xb,Xp)
| Xa = Xb )
& ! [Xa,Xb] :
( ! [Xp] : s_col(Xa,Xb,midpoint(Xp,reflect(Xa,Xb,Xp)))
| Xa = Xb ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f539,plain,
! [X0,X1,X2] :
( X1 = X0
| s_col(X0,X1,midpoint(X2,reflect(X0,X1,X2))) ),
inference(cnf_transformation,[status(thm)],[f538]) ).
fof(f544,plain,
! [X0,X1,X2,X3] :
( reflect(X0,X1,X3) = X2
| reflect(X0,X1,X2) != X3
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f550,plain,
! [X0,X1,X2] :
( reflect(X0,X1,X2) != X2
| X0 = X1
| s_col(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f551,plain,
! [X0,X1,X2] :
( X0 = X1
| X2 = reflect(X0,X1,X2)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f564,plain,
? [Xa,Xb,Xp,Xp1] :
( ~ opposite(Xp,Xa,Xb,Xp1)
& ~ s_col(Xa,Xb,Xp)
& reflect(Xa,Xb,Xp) = Xp1
& Xa != Xb ),
inference(pre_NNF_transformation,[status(thm)],[f199]) ).
fof(f565,plain,
( ~ opposite(sK2_skl,sK0_skl,sK1_skl,sK3_skl)
& ~ s_col(sK0_skl,sK1_skl,sK2_skl)
& reflect(sK0_skl,sK1_skl,sK2_skl) = sK3_skl
& sK0_skl != sK1_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(Xa,sK0_skl),skolemize(Xb,sK1_skl),skolemize(Xp,sK2_skl),skolemize(Xp1,sK3_skl)],[f564]) ).
fof(f566,plain,
sK0_skl != sK1_skl,
inference(cnf_transformation,[status(thm)],[f565]) ).
fof(f567,plain,
sK3_skl = reflect(sK0_skl,sK1_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f565]) ).
fof(f568,plain,
~ s_col(sK0_skl,sK1_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f565]) ).
fof(f569,plain,
~ opposite(sK2_skl,sK0_skl,sK1_skl,sK3_skl),
inference(cnf_transformation,[status(thm)],[f565]) ).
fof(f613,plain,
( ! [Xa,Xm,Xb] :
( s_m(Xa,Xm,Xb)
| ~ s_e(Xm,Xa,Xm,Xb)
| ~ s_t(Xa,Xm,Xb) )
& ! [Xa,Xm,Xb] :
( s_e(Xm,Xa,Xm,Xb)
| ~ s_m(Xa,Xm,Xb) )
& ! [Xa,Xm,Xb] :
( s_t(Xa,Xm,Xb)
| ~ s_m(Xa,Xm,Xb) ) ),
inference(miniscoping,[status(thm)],[f208]) ).
fof(f614,plain,
! [X0,X1,X2] :
( s_t(X0,X1,X2)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f613]) ).
fof(f640,plain,
( ! [Xp,Xq,Xa,Xb] :
( s_col(Xp,Xq,il(Xa,Xb,Xp,Xq))
| ~ opposite(Xa,Xp,Xq,Xb) )
& ! [Xp,Xq,Xa,Xb] :
( s_t(Xa,il(Xa,Xb,Xp,Xq),Xb)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ! [Xp,Xq,Xb] :
( ~ s_col(Xp,Xq,Xb)
| ! [Xa] : ~ opposite(Xa,Xp,Xq,Xb) )
& ! [Xp,Xq,Xa] :
( ~ s_col(Xp,Xq,Xa)
| ! [Xb] : ~ opposite(Xa,Xp,Xq,Xb) )
& ! [Xp,Xq,Xa,Xb] :
( opposite(Xa,Xp,Xq,Xb)
| ! [Xt] :
( ~ s_col(Xp,Xq,Xt)
| ~ s_t(Xa,Xt,Xb)
| s_col(Xp,Xq,Xb)
| s_col(Xp,Xq,Xa)
| Xp = Xq ) ) ),
inference(miniscoping,[status(thm)],[f213]) ).
fof(f641,plain,
! [X0,X1,X2,X3,X4] :
( s_col(X1,X2,X3)
| X1 = X2
| ~ s_t(X0,X4,X3)
| s_col(X1,X2,X0)
| ~ s_col(X1,X2,X4)
| opposite(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f640]) ).
fof(f685,plain,
! [X0,X1,X2] :
( X0 = X1
| reflect(X0,X1,reflect(X0,X1,X2)) = X2 ),
inference(destructive_equality_resolution,[status(thm)],[f544]) ).
fof(f713,plain,
~ s_col(sK2_skl,sK0_skl,sK1_skl),
inference(resolution,[status(thm)],[f281,f568]) ).
fof(f718,definition,
( sQ9_spl
<=> sK0_skl = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f719,plain,
( ~ sQ9_spl
| sK0_skl = sK1_skl ),
inference(component_clause,[status(thm)],[f718]) ).
fof(f722,plain,
( ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f719,f566]) ).
fof(f723,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f722]) ).
fof(f725,plain,
~ s_col(sK1_skl,sK2_skl,sK0_skl),
inference(resolution,[status(thm)],[f713,f281]) ).
fof(f729,definition,
( sQ11_spl
<=> sK2_skl = sK0_skl ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f730,plain,
( ~ sQ11_spl
| sK2_skl = sK0_skl ),
inference(component_clause,[status(thm)],[f729]) ).
fof(f733,plain,
( ~ sQ11_spl
| ~ s_col(sK0_skl,sK0_skl,sK1_skl) ),
inference(backward_demodulation,[status(thm)],[f730,f713]) ).
fof(f736,plain,
( ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f733,f286]) ).
fof(f737,plain,
~ sQ11_spl,
inference(contradiction_clause,[status(thm)],[f736]) ).
fof(f744,definition,
( sQ13_spl
<=> sK2_skl = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f745,plain,
( ~ sQ13_spl
| sK2_skl = sK1_skl ),
inference(component_clause,[status(thm)],[f744]) ).
fof(f752,plain,
( ~ sQ13_spl
| ~ s_col(sK1_skl,sK1_skl,sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f745,f725]) ).
fof(f754,plain,
( ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f752,f286]) ).
fof(f755,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f754]) ).
fof(f757,plain,
~ s_col(sK1_skl,sK0_skl,sK2_skl),
inference(resolution,[status(thm)],[f713,f283]) ).
fof(f801,plain,
( sK0_skl = sK1_skl
| ~ s_col(sK0_skl,sK1_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f757,f364]) ).
fof(f804,definition,
( sQ19_spl
<=> s_col(sK0_skl,sK1_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f807,plain,
( sQ9_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f801,f804,f718]) ).
fof(f853,definition,
( sQ24_spl
<=> s_col(sK2_skl,sK2_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f855,plain,
( sQ24_spl
| ~ s_col(sK2_skl,sK2_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f853]) ).
fof(f857,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f855,f286]) ).
fof(f858,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f857]) ).
fof(f866,definition,
( sQ25_spl
<=> s_col(sK0_skl,sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f868,plain,
( sQ25_spl
| ~ s_col(sK0_skl,sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f866]) ).
fof(f874,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f868,f286]) ).
fof(f875,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f874]) ).
fof(f892,plain,
! [X0,X1] : s_col(X0,X1,X1),
inference(resolution,[status(thm)],[f282,f286]) ).
fof(f920,plain,
( sK0_skl = sK1_skl
| reflect(sK0_skl,sK1_skl,sK3_skl) = sK2_skl ),
inference(paramodulation,[status(thm)],[f567,f685]) ).
fof(f922,definition,
( sQ28_spl
<=> reflect(sK0_skl,sK1_skl,sK3_skl) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f923,plain,
( ~ sQ28_spl
| reflect(sK0_skl,sK1_skl,sK3_skl) = sK2_skl ),
inference(component_clause,[status(thm)],[f922]) ).
fof(f925,plain,
( sQ9_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f920,f922,f718]) ).
fof(f942,definition,
( sQ30_spl
<=> s_t(gamma,beta,alpha) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f943,plain,
( ~ sQ30_spl
| s_t(gamma,beta,alpha) ),
inference(component_clause,[status(thm)],[f942]) ).
fof(f949,definition,
( sQ32_spl
<=> s_t(alpha,gamma,beta) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f950,plain,
( ~ sQ32_spl
| s_t(alpha,gamma,beta) ),
inference(component_clause,[status(thm)],[f949]) ).
fof(f956,definition,
( sQ34_spl
<=> s_t(beta,alpha,gamma) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f957,plain,
( ~ sQ34_spl
| s_t(beta,alpha,gamma) ),
inference(component_clause,[status(thm)],[f956]) ).
fof(f973,definition,
( sQ37_spl
<=> s_col(sK1_skl,sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f975,plain,
( sQ37_spl
| ~ s_col(sK1_skl,sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f973]) ).
fof(f979,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f975,f286]) ).
fof(f980,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f979]) ).
fof(f985,plain,
( sK1_skl = sK0_skl
| s_col(sK0_skl,sK1_skl,midpoint(sK2_skl,sK3_skl)) ),
inference(paramodulation,[status(thm)],[f567,f539]) ).
fof(f995,definition,
( sQ40_spl
<=> s_col(sK0_skl,sK1_skl,midpoint(sK2_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f996,plain,
( ~ sQ40_spl
| s_col(sK0_skl,sK1_skl,midpoint(sK2_skl,sK3_skl)) ),
inference(component_clause,[status(thm)],[f995]) ).
fof(f998,plain,
( sQ9_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f985,f995,f718]) ).
fof(f1058,definition,
( sQ46_spl
<=> s_col(sK0_skl,sK1_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1059,plain,
( ~ sQ46_spl
| s_col(sK0_skl,sK1_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f1058]) ).
fof(f1086,plain,
~ s_t(gamma,beta,alpha),
inference(resolution,[status(thm)],[f248,f229]) ).
fof(f1087,plain,
~ s_t(alpha,gamma,beta),
inference(resolution,[status(thm)],[f248,f230]) ).
fof(f1088,plain,
~ s_t(beta,alpha,gamma),
inference(resolution,[status(thm)],[f248,f231]) ).
fof(f1091,plain,
( ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1087,f950]) ).
fof(f1092,plain,
~ sQ32_spl,
inference(contradiction_clause,[status(thm)],[f1091]) ).
fof(f1093,plain,
( ~ sQ34_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1088,f957]) ).
fof(f1094,plain,
~ sQ34_spl,
inference(contradiction_clause,[status(thm)],[f1093]) ).
fof(f1095,plain,
( ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1086,f943]) ).
fof(f1096,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1095]) ).
fof(f1102,definition,
( sQ49_spl
<=> s_t(alpha,beta,gamma) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f1103,plain,
( ~ sQ49_spl
| s_t(alpha,beta,gamma) ),
inference(component_clause,[status(thm)],[f1102]) ).
fof(f1106,plain,
( ~ sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1103,f229]) ).
fof(f1107,plain,
~ sQ49_spl,
inference(contradiction_clause,[status(thm)],[f1106]) ).
fof(f1119,definition,
( sQ50_spl
<=> s_t(beta,gamma,alpha) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1120,plain,
( ~ sQ50_spl
| s_t(beta,gamma,alpha) ),
inference(component_clause,[status(thm)],[f1119]) ).
fof(f1123,plain,
( ~ sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1120,f230]) ).
fof(f1124,plain,
~ sQ50_spl,
inference(contradiction_clause,[status(thm)],[f1123]) ).
fof(f1138,definition,
( sQ51_spl
<=> s_t(gamma,alpha,beta) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1139,plain,
( ~ sQ51_spl
| s_t(gamma,alpha,beta) ),
inference(component_clause,[status(thm)],[f1138]) ).
fof(f1142,plain,
( ~ sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1139,f231]) ).
fof(f1143,plain,
~ sQ51_spl,
inference(contradiction_clause,[status(thm)],[f1142]) ).
fof(f1196,plain,
( reflect(sK0_skl,sK1_skl,sK2_skl) != sK2_skl
| sK0_skl = sK1_skl ),
inference(resolution,[status(thm)],[f550,f568]) ).
fof(f1226,definition,
( sQ63_spl
<=> reflect(sK0_skl,sK1_skl,sK2_skl) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1228,plain,
( sQ63_spl
| reflect(sK0_skl,sK1_skl,sK2_skl) != sK2_skl ),
inference(component_clause,[status(thm)],[f1226]) ).
fof(f1229,plain,
( ~ sQ63_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f1196,f718,f1226]) ).
fof(f1240,plain,
( sQ63_spl
| sK3_skl != sK2_skl ),
inference(forward_demodulation,[status(thm)],[f567,f1228]) ).
fof(f1280,definition,
( sQ72_spl
<=> gamma = alpha ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1281,plain,
( ~ sQ72_spl
| gamma = alpha ),
inference(component_clause,[status(thm)],[f1280]) ).
fof(f1288,plain,
( ~ sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1281,f266]) ).
fof(f1289,plain,
~ sQ72_spl,
inference(contradiction_clause,[status(thm)],[f1288]) ).
fof(f1421,definition,
( sQ94_spl
<=> beta = gamma ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1422,plain,
( ~ sQ94_spl
| beta = gamma ),
inference(component_clause,[status(thm)],[f1421]) ).
fof(f1429,plain,
( ~ sQ94_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1422,f265]) ).
fof(f1430,plain,
~ sQ94_spl,
inference(contradiction_clause,[status(thm)],[f1429]) ).
fof(f1437,definition,
( sQ96_spl
<=> reflect(sK0_skl,sK1_skl,sK3_skl) = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f1438,plain,
( ~ sQ96_spl
| reflect(sK0_skl,sK1_skl,sK3_skl) = sK3_skl ),
inference(component_clause,[status(thm)],[f1437]) ).
fof(f1525,definition,
( sQ104_spl
<=> beta = alpha ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1526,plain,
( ~ sQ104_spl
| beta = alpha ),
inference(component_clause,[status(thm)],[f1525]) ).
fof(f1536,plain,
( ~ sQ104_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1526,f264]) ).
fof(f1537,plain,
~ sQ104_spl,
inference(contradiction_clause,[status(thm)],[f1536]) ).
fof(f1822,plain,
! [X0] :
( s_col(sK0_skl,sK1_skl,sK3_skl)
| sK0_skl = sK1_skl
| ~ s_t(sK2_skl,X0,sK3_skl)
| s_col(sK0_skl,sK1_skl,sK2_skl)
| ~ s_col(sK0_skl,sK1_skl,X0) ),
inference(resolution,[status(thm)],[f641,f569]) ).
fof(f1832,definition,
! [X0] :
( sQ118_spl
<=> ( ~ s_t(sK2_skl,X0,sK3_skl)
| ~ s_col(sK0_skl,sK1_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f1833,plain,
! [X0] :
( ~ sQ118_spl
| ~ s_t(sK2_skl,X0,sK3_skl)
| ~ s_col(sK0_skl,sK1_skl,X0) ),
inference(component_clause,[status(thm)],[f1832]) ).
fof(f1835,plain,
( sQ46_spl
| sQ9_spl
| sQ19_spl
| sQ118_spl ),
inference(split_clause,[status(thm)],[f1822,f1832,f804,f718,f1058]) ).
fof(f1899,definition,
( sQ121_spl
<=> s_col(sK0_skl,sK1_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1901,plain,
( sQ121_spl
| ~ s_col(sK0_skl,sK1_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f1899]) ).
fof(f1906,definition,
( sQ123_spl
<=> s_col(sK0_skl,sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1908,plain,
( sQ123_spl
| ~ s_col(sK0_skl,sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f1906]) ).
fof(f1910,plain,
( sQ121_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1901,f892]) ).
fof(f1911,plain,
sQ121_spl,
inference(contradiction_clause,[status(thm)],[f1910]) ).
fof(f1912,plain,
( sQ123_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1908,f287]) ).
fof(f1913,plain,
sQ123_spl,
inference(contradiction_clause,[status(thm)],[f1912]) ).
fof(f2027,plain,
! [X0,X1] : s_t(X0,midpoint(X0,X1),X1),
inference(resolution,[status(thm)],[f614,f470]) ).
fof(f2281,plain,
( ~ sQ118_spl
| ~ sQ40_spl
| ~ s_t(sK2_skl,midpoint(sK2_skl,sK3_skl),sK3_skl) ),
inference(resolution,[status(thm)],[f996,f1833]) ).
fof(f2295,plain,
( ~ sQ118_spl
| ~ sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2281,f2027]) ).
fof(f2296,plain,
( ~ sQ118_spl
| ~ sQ40_spl ),
inference(contradiction_clause,[status(thm)],[f2295]) ).
fof(f2343,definition,
( sQ142_spl
<=> s_col(sK0_skl,sK0_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f2345,plain,
( sQ142_spl
| ~ s_col(sK0_skl,sK0_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f2343]) ).
fof(f2354,plain,
( sQ142_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2345,f286]) ).
fof(f2355,plain,
sQ142_spl,
inference(contradiction_clause,[status(thm)],[f2354]) ).
fof(f2388,plain,
( ~ sQ46_spl
| sK0_skl = sK1_skl
| sK3_skl = reflect(sK0_skl,sK1_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f1059,f551]) ).
fof(f2395,plain,
( ~ sQ46_spl
| sQ9_spl
| sQ96_spl ),
inference(split_clause,[status(thm)],[f2388,f1437,f718,f1058]) ).
fof(f2404,plain,
( ~ sQ96_spl
| ~ sQ28_spl
| sK2_skl = sK3_skl ),
inference(forward_demodulation,[status(thm)],[f923,f1438]) ).
fof(f2405,plain,
( ~ sQ96_spl
| ~ sQ28_spl
| sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2404,f1240]) ).
fof(f2406,plain,
( ~ sQ96_spl
| ~ sQ28_spl
| sQ63_spl ),
inference(contradiction_clause,[status(thm)],[f2405]) ).
fof(f2407,plain,
$false,
inference(sat_refutation,[status(thm)],[f723,f737,f755,f807,f858,f875,f925,f980,f998,f1092,f1094,f1096,f1107,f1124,f1143,f1229,f1289,f1430,f1537,f1835,f1911,f1913,f2296,f2355,f2395,f2406]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO528+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.58 % Computer : n018.cluster.edu
% 0.09/0.58 % Model : x86_64 x86_64
% 0.09/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.58 % Memory : 8046.5625MB
% 0.09/0.58 % OS : Linux 6.8.0-71-generic
% 0.09/0.58 % CPULimit : 300
% 0.09/0.58 % WCLimit : 300
% 0.09/0.58 % DateTime : Sun Sep 20 17:15:13 UTC 2026
% 0.15/0.58 % CPUTime :
% 0.15/0.61 % Drodi V4.1.1
% 53.79/7.47 % Refutation found
% 53.79/7.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 53.79/7.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.17/7.50 % Elapsed time: 6.905688 seconds
% 6.17/7.50 % CPU time: 54.432772 seconds
% 6.17/7.50 % Total memory used: 217.381 MB
% 6.17/7.50 % Net memory used: 200.119 MB
%------------------------------------------------------------------------------