%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO535+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 : 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:25:11 PM UTC 2026
% Result : Theorem 33.59s 8.31s
% Output : CNFRefutation 33.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 14
% Syntax : Number of formulae : 69 ( 14 unt; 8 def)
% Number of atoms : 204 ( 17 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 243 ( 108 ~; 102 |; 25 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 9 prp; 0-6 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-4 aty)
% Number of variables : 161 ( 149 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f70,axiom,
! [Xa,Xp,Xb] :
( ( s_t(Xb,Xp,c63(Xa,Xp,Xb))
| ~ sameside(Xa,Xp,Xb) )
& ( s_t(Xa,Xp,c63(Xa,Xp,Xb))
| ~ sameside(Xa,Xp,Xb) )
& ( c63(Xa,Xp,Xb) != Xp
| ~ sameside(Xa,Xp,Xb) )
& ( Xb != Xp
| ~ sameside(Xa,Xp,Xb) )
& ( Xa != Xp
| ~ sameside(Xa,Xp,Xb) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [Xa,Xp] :
( sameside(Xa,Xp,Xa)
| Xa = Xp ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f202,axiom,
! [Xa,Xb,Xc,Xd,Xe,Xf] :
( ( s_e3(ext(Xb,Xa,Xe,Xd),Xb,ext(Xb,Xc,Xe,Xf),ext(Xe,Xd,Xb,Xa),Xe,ext(Xe,Xf,Xb,Xc))
| ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) )
& ( sameside(ext(Xe,Xf,Xb,Xc),Xe,Xf)
| ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) )
& ( sameside(ext(Xe,Xd,Xb,Xa),Xe,Xd)
| ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) )
& ( sameside(ext(Xb,Xc,Xe,Xf),Xb,Xc)
| ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) )
& ( sameside(ext(Xb,Xa,Xe,Xd),Xb,Xa)
| ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f205,axiom,
! [Xa,Xb,Xc,Xd,Xe,Xf,Xa2,Xc2,Xd2,Xf2] :
( s_e(Xa2,Xc2,Xd2,Xf2)
| ~ s_e(Xb,Xc2,Xe,Xf2)
| ~ s_e(Xb,Xa2,Xe,Xd2)
| ~ sameside(Xf2,Xe,Xf)
| ~ sameside(Xd2,Xe,Xd)
| ~ sameside(Xc2,Xb,Xc)
| ~ sameside(Xa2,Xb,Xa)
| ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f208,axiom,
! [Xa,Xb,Xc,Xd,Xe,Xf] :
( congruent(Xd,Xe,Xf,Xa,Xb,Xc)
| ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f213,conjecture,
! [Xa,Xb,Xc,Xa1,Xb1,Xc1] :
( s_e(Xa,Xc,Xa1,Xc1)
| ~ s_e(Xb,Xc,Xb1,Xc1)
| ~ s_e(Xb,Xa,Xb1,Xa1)
| ~ congruent(Xa,Xb,Xc,Xa1,Xb1,Xc1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f214,negated_conjecture,
~ ! [Xa,Xb,Xc,Xa1,Xb1,Xc1] :
( s_e(Xa,Xc,Xa1,Xc1)
| ~ s_e(Xb,Xc,Xb1,Xc1)
| ~ s_e(Xb,Xa,Xb1,Xa1)
| ~ congruent(Xa,Xb,Xc,Xa1,Xb1,Xc1) ),
inference(negated_conjecture,[status(cth)],[f213]) ).
fof(f343,plain,
( ! [Xa,Xp,Xb] :
( s_t(Xb,Xp,c63(Xa,Xp,Xb))
| ~ sameside(Xa,Xp,Xb) )
& ! [Xa,Xp,Xb] :
( s_t(Xa,Xp,c63(Xa,Xp,Xb))
| ~ sameside(Xa,Xp,Xb) )
& ! [Xa,Xp,Xb] :
( c63(Xa,Xp,Xb) != Xp
| ~ sameside(Xa,Xp,Xb) )
& ! [Xp,Xb] :
( Xb != Xp
| ! [Xa] : ~ sameside(Xa,Xp,Xb) )
& ! [Xa,Xp] :
( Xa != Xp
| ! [Xb] : ~ sameside(Xa,Xp,Xb) ) ),
inference(miniscoping,[status(thm)],[f70]) ).
fof(f345,plain,
! [X0,X1,X2] :
( X2 != X1
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f343]) ).
fof(f355,plain,
! [X0,X1] :
( sameside(X0,X1,X0)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f588,plain,
( ! [Xa,Xb,Xc,Xd,Xe,Xf] :
( s_e3(ext(Xb,Xa,Xe,Xd),Xb,ext(Xb,Xc,Xe,Xf),ext(Xe,Xd,Xb,Xa),Xe,ext(Xe,Xf,Xb,Xc))
| ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) )
& ! [Xb,Xc,Xe,Xf] :
( sameside(ext(Xe,Xf,Xb,Xc),Xe,Xf)
| ! [Xa,Xd] : ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) )
& ! [Xa,Xb,Xd,Xe] :
( sameside(ext(Xe,Xd,Xb,Xa),Xe,Xd)
| ! [Xc,Xf] : ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) )
& ! [Xb,Xc,Xe,Xf] :
( sameside(ext(Xb,Xc,Xe,Xf),Xb,Xc)
| ! [Xa,Xd] : ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) )
& ! [Xa,Xb,Xd,Xe] :
( sameside(ext(Xb,Xa,Xe,Xd),Xb,Xa)
| ! [Xc,Xf] : ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) ) ),
inference(miniscoping,[status(thm)],[f202]) ).
fof(f591,plain,
! [X0,X1,X2,X3,X4,X5] :
( sameside(ext(X4,X3,X1,X0),X4,X3)
| ~ congruent(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(thm)],[f588]) ).
fof(f592,plain,
! [X0,X1,X2,X3,X4,X5] :
( sameside(ext(X4,X5,X1,X2),X4,X5)
| ~ congruent(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(thm)],[f588]) ).
fof(f604,plain,
! [Xa2,Xc2,Xd2,Xf2] :
( s_e(Xa2,Xc2,Xd2,Xf2)
| ! [Xb,Xe] :
( ~ s_e(Xb,Xc2,Xe,Xf2)
| ~ s_e(Xb,Xa2,Xe,Xd2)
| ! [Xf] :
( ~ sameside(Xf2,Xe,Xf)
| ! [Xd] :
( ~ sameside(Xd2,Xe,Xd)
| ! [Xc] :
( ~ sameside(Xc2,Xb,Xc)
| ! [Xa] :
( ~ sameside(Xa2,Xb,Xa)
| ~ congruent(Xa,Xb,Xc,Xd,Xe,Xf) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f205]) ).
fof(f605,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( s_e(X6,X7,X8,X9)
| ~ s_e(X1,X7,X4,X9)
| ~ s_e(X1,X6,X4,X8)
| ~ sameside(X9,X4,X5)
| ~ sameside(X8,X4,X3)
| ~ sameside(X7,X1,X2)
| ~ sameside(X6,X1,X0)
| ~ congruent(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(thm)],[f604]) ).
fof(f609,plain,
! [X0,X1,X2,X3,X4,X5] :
( congruent(X3,X4,X5,X0,X1,X2)
| ~ congruent(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f618,plain,
? [Xa,Xb,Xc,Xa1,Xb1,Xc1] :
( ~ s_e(Xa,Xc,Xa1,Xc1)
& s_e(Xb,Xc,Xb1,Xc1)
& s_e(Xb,Xa,Xb1,Xa1)
& congruent(Xa,Xb,Xc,Xa1,Xb1,Xc1) ),
inference(pre_NNF_transformation,[status(thm)],[f214]) ).
fof(f619,plain,
? [Xa,Xc,Xa1,Xc1] :
( ~ s_e(Xa,Xc,Xa1,Xc1)
& ? [Xb,Xb1] :
( s_e(Xb,Xc,Xb1,Xc1)
& s_e(Xb,Xa,Xb1,Xa1)
& congruent(Xa,Xb,Xc,Xa1,Xb1,Xc1) ) ),
inference(miniscoping,[status(thm)],[f618]) ).
fof(f620,plain,
( ~ s_e(sK0_skl,sK1_skl,sK2_skl,sK3_skl)
& s_e(sK4_skl,sK1_skl,sK5_skl,sK3_skl)
& s_e(sK4_skl,sK0_skl,sK5_skl,sK2_skl)
& congruent(sK0_skl,sK4_skl,sK1_skl,sK2_skl,sK5_skl,sK3_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(Xa,sK0_skl),skolemize(Xc,sK1_skl),skolemize(Xa1,sK2_skl),skolemize(Xc1,sK3_skl),skolemize(Xb,sK4_skl),skolemize(Xb1,sK5_skl)],[f619]) ).
fof(f621,plain,
congruent(sK0_skl,sK4_skl,sK1_skl,sK2_skl,sK5_skl,sK3_skl),
inference(cnf_transformation,[status(thm)],[f620]) ).
fof(f622,plain,
s_e(sK4_skl,sK0_skl,sK5_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f620]) ).
fof(f623,plain,
s_e(sK4_skl,sK1_skl,sK5_skl,sK3_skl),
inference(cnf_transformation,[status(thm)],[f620]) ).
fof(f624,plain,
~ s_e(sK0_skl,sK1_skl,sK2_skl,sK3_skl),
inference(cnf_transformation,[status(thm)],[f620]) ).
fof(f734,plain,
! [X0,X1] : ~ sameside(X0,X1,X1),
inference(destructive_equality_resolution,[status(thm)],[f345]) ).
fof(f970,plain,
congruent(sK2_skl,sK5_skl,sK3_skl,sK0_skl,sK4_skl,sK1_skl),
inference(resolution,[status(thm)],[f609,f621]) ).
fof(f1261,plain,
! [X0,X1,X2,X3] :
( s_e(X0,X1,X2,X3)
| ~ s_e(sK4_skl,X1,sK5_skl,X3)
| ~ s_e(sK4_skl,X0,sK5_skl,X2)
| ~ sameside(X3,sK5_skl,sK3_skl)
| ~ sameside(X2,sK5_skl,sK2_skl)
| ~ sameside(X1,sK4_skl,sK1_skl)
| ~ sameside(X0,sK4_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f605,f621]) ).
fof(f1322,definition,
( sQ57_spl
<=> sK1_skl = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1323,plain,
( ~ sQ57_spl
| sK1_skl = sK4_skl ),
inference(component_clause,[status(thm)],[f1322]) ).
fof(f1539,definition,
( sQ59_spl
<=> sK4_skl = sK0_skl ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1540,plain,
( ~ sQ59_spl
| sK4_skl = sK0_skl ),
inference(component_clause,[status(thm)],[f1539]) ).
fof(f1582,plain,
( ~ sQ59_spl
| congruent(sK2_skl,sK5_skl,sK3_skl,sK0_skl,sK0_skl,sK1_skl) ),
inference(backward_demodulation,[status(thm)],[f1540,f970]) ).
fof(f1812,plain,
( ~ sQ57_spl
| congruent(sK2_skl,sK5_skl,sK3_skl,sK0_skl,sK1_skl,sK1_skl) ),
inference(backward_demodulation,[status(thm)],[f1323,f970]) ).
fof(f2217,definition,
( sQ77_spl
<=> sameside(sK3_skl,sK5_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f2219,plain,
( sQ77_spl
| ~ sameside(sK3_skl,sK5_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f2217]) ).
fof(f2777,plain,
! [X0,X1,X2,X3,X4] : ~ congruent(X0,X1,X2,X3,X3,X4),
inference(resolution,[status(thm)],[f591,f734]) ).
fof(f2785,plain,
! [X0,X1,X2,X3,X4] : ~ congruent(X0,X1,X2,X3,X4,X4),
inference(resolution,[status(thm)],[f592,f734]) ).
fof(f2894,definition,
( sQ103_spl
<=> s_e(sK0_skl,sK1_skl,sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f2895,plain,
( ~ sQ103_spl
| s_e(sK0_skl,sK1_skl,sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f2894]) ).
fof(f2901,plain,
( ~ sQ103_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2895,f624]) ).
fof(f2902,plain,
~ sQ103_spl,
inference(contradiction_clause,[status(thm)],[f2901]) ).
fof(f3097,plain,
! [X0,X1] :
( s_e(X0,sK1_skl,X1,sK3_skl)
| ~ s_e(sK4_skl,X0,sK5_skl,X1)
| ~ sameside(sK3_skl,sK5_skl,sK3_skl)
| ~ sameside(X1,sK5_skl,sK2_skl)
| ~ sameside(sK1_skl,sK4_skl,sK1_skl)
| ~ sameside(X0,sK4_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f1261,f623]) ).
fof(f3103,definition,
! [X0,X1] :
( sQ114_spl
<=> ( s_e(X0,sK1_skl,X1,sK3_skl)
| ~ s_e(sK4_skl,X0,sK5_skl,X1)
| ~ sameside(X1,sK5_skl,sK2_skl)
| ~ sameside(X0,sK4_skl,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition]) ).
fof(f3104,plain,
! [X0,X1] :
( ~ sQ114_spl
| s_e(X0,sK1_skl,X1,sK3_skl)
| ~ s_e(sK4_skl,X0,sK5_skl,X1)
| ~ sameside(X1,sK5_skl,sK2_skl)
| ~ sameside(X0,sK4_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f3103]) ).
fof(f3106,definition,
( sQ115_spl
<=> sameside(sK1_skl,sK4_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f3108,plain,
( sQ115_spl
| ~ sameside(sK1_skl,sK4_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f3106]) ).
fof(f3109,plain,
( ~ sQ77_spl
| ~ sQ115_spl
| sQ114_spl ),
inference(split_clause,[status(thm)],[f3097,f3103,f3106,f2217]) ).
fof(f3206,plain,
( sQ115_spl
| sK1_skl = sK4_skl ),
inference(resolution,[status(thm)],[f3108,f355]) ).
fof(f3208,plain,
( sQ115_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f3206,f1322,f3106]) ).
fof(f3317,definition,
( sQ127_spl
<=> sameside(sK0_skl,sK4_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition]) ).
fof(f3319,plain,
( sQ127_spl
| ~ sameside(sK0_skl,sK4_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f3317]) ).
fof(f3320,definition,
( sQ128_spl
<=> sameside(sK2_skl,sK5_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition]) ).
fof(f3322,plain,
( sQ128_spl
| ~ sameside(sK2_skl,sK5_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f3320]) ).
fof(f3345,plain,
( sQ128_spl
| sK2_skl = sK5_skl ),
inference(resolution,[status(thm)],[f3322,f355]) ).
fof(f3355,plain,
( sQ127_spl
| sK0_skl = sK4_skl ),
inference(resolution,[status(thm)],[f3319,f355]) ).
fof(f3359,plain,
( ~ sQ114_spl
| s_e(sK0_skl,sK1_skl,sK2_skl,sK3_skl)
| ~ sameside(sK2_skl,sK5_skl,sK2_skl)
| ~ sameside(sK0_skl,sK4_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f3104,f622]) ).
fof(f3365,plain,
( ~ sQ114_spl
| sQ103_spl
| ~ sQ128_spl
| ~ sQ127_spl ),
inference(split_clause,[status(thm)],[f3359,f3317,f3320,f2894,f3103]) ).
fof(f3368,plain,
( sQ127_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f3355,f1539,f3317]) ).
fof(f3405,plain,
( sQ128_spl
| congruent(sK0_skl,sK4_skl,sK1_skl,sK2_skl,sK2_skl,sK3_skl) ),
inference(backward_demodulation,[status(thm)],[f3345,f621]) ).
fof(f3522,plain,
( ~ sQ59_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1582,f2777]) ).
fof(f3523,plain,
~ sQ59_spl,
inference(contradiction_clause,[status(thm)],[f3522]) ).
fof(f3525,plain,
( ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1812,f2785]) ).
fof(f3526,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f3525]) ).
fof(f3533,plain,
( sQ128_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3405,f2777]) ).
fof(f3534,plain,
sQ128_spl,
inference(contradiction_clause,[status(thm)],[f3533]) ).
fof(f3789,plain,
( sQ77_spl
| sK3_skl = sK5_skl ),
inference(resolution,[status(thm)],[f2219,f355]) ).
fof(f3820,plain,
( sQ77_spl
| congruent(sK0_skl,sK4_skl,sK1_skl,sK2_skl,sK3_skl,sK3_skl) ),
inference(backward_demodulation,[status(thm)],[f3789,f621]) ).
fof(f3937,plain,
( sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3820,f2785]) ).
fof(f3938,plain,
sQ77_spl,
inference(contradiction_clause,[status(thm)],[f3937]) ).
fof(f3939,plain,
$false,
inference(sat_refutation,[status(thm)],[f2902,f3109,f3208,f3365,f3368,f3523,f3526,f3534,f3938]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO535+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/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 17:23:00 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.40 % Drodi V4.1.1
% 33.59/8.31 % Refutation found
% 33.59/8.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 33.59/8.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 33.59/8.33 % Elapsed time: 7.939446 seconds
% 33.59/8.33 % CPU time: 62.622295 seconds
% 33.59/8.33 % Total memory used: 240.923 MB
% 33.59/8.33 % Net memory used: 209.379 MB
%------------------------------------------------------------------------------