%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO523+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 60.48s 8.08s
% Output : CNFRefutation 60.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 13
% Syntax : Number of formulae : 57 ( 14 unt; 5 def)
% Number of atoms : 132 ( 64 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 122 ( 47 ~; 62 |; 8 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 6 prp; 0-4 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-3 aty)
% Number of variables : 89 ( 85 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f93,axiom,
! [Xa,Xm,Xb] :
( s_m(Xb,Xm,Xa)
| ~ s_m(Xa,Xm,Xb) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [Xp,Xa,Xq] :
( Xq = s(Xa,Xp)
| ~ s_m(Xp,Xa,Xq) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f110,axiom,
! [Xa,Xp,Xb] :
( Xa = Xb
| s(Xa,Xp) != s(Xb,Xp) ),
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(f154,axiom,
! [Xa,Xb,Xp,Xq] :
( perp(Xa,Xb,Xq,Xp)
| ~ perp(Xa,Xb,Xp,Xq) ),
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(f185,axiom,
! [Xa,Xb,Xp,Xp1] :
( ( Xp1 = reflect(Xa,Xb,Xp)
| Xp != Xp1
| ~ s_col(Xa,Xb,midpoint(Xp,Xp1))
| Xa = Xb )
& ( Xp1 = reflect(Xa,Xb,Xp)
| ~ perp(Xa,Xb,Xp,Xp1)
| ~ s_col(Xa,Xb,midpoint(Xp,Xp1))
| Xa = Xb ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f186,conjecture,
! [Xa,Xb,Xp,Xp1] :
( reflect(Xa,Xb,Xp1) = Xp
| reflect(Xa,Xb,Xp) != Xp1
| Xa = Xb ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f187,negated_conjecture,
~ ! [Xa,Xb,Xp,Xp1] :
( reflect(Xa,Xb,Xp1) = Xp
| reflect(Xa,Xb,Xp) != Xp1
| Xa = Xb ),
inference(negated_conjecture,[status(cth)],[f186]) ).
fof(f360,plain,
! [X0,X1,X2] :
( s_m(X2,X1,X0)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f366,plain,
! [X0,X1,X2] :
( X2 = s(X1,X0)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f385,plain,
! [Xa,Xb] :
( Xa = Xb
| ! [Xp] : s(Xa,Xp) != s(Xb,Xp) ),
inference(miniscoping,[status(thm)],[f110]) ).
fof(f386,plain,
! [X0,X1,X2] :
( X0 = X2
| s(X0,X1) != s(X2,X1) ),
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f458,plain,
! [X0,X1] : s_m(X0,midpoint(X0,X1),X1),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f473,plain,
! [X0,X1,X2,X3] :
( perp(X0,X1,X3,X2)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f526,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(f527,plain,
! [X0,X1,X2] :
( s_col(X0,X1,midpoint(X2,reflect(X0,X1,X2)))
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f526]) ).
fof(f528,plain,
! [X0,X1,X2] :
( perp(X0,X1,X2,reflect(X0,X1,X2))
| X2 = reflect(X0,X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f526]) ).
fof(f529,plain,
( ! [Xa,Xb,Xp,Xp1] :
( Xp1 = reflect(Xa,Xb,Xp)
| Xp != Xp1
| ~ s_col(Xa,Xb,midpoint(Xp,Xp1))
| Xa = Xb )
& ! [Xa,Xb,Xp,Xp1] :
( Xp1 = reflect(Xa,Xb,Xp)
| ~ perp(Xa,Xb,Xp,Xp1)
| ~ s_col(Xa,Xb,midpoint(Xp,Xp1))
| Xa = Xb ) ),
inference(miniscoping,[status(thm)],[f185]) ).
fof(f530,plain,
! [X0,X1,X2,X3] :
( X3 = reflect(X0,X1,X2)
| ~ perp(X0,X1,X2,X3)
| ~ s_col(X0,X1,midpoint(X2,X3))
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f529]) ).
fof(f532,plain,
? [Xa,Xb,Xp,Xp1] :
( reflect(Xa,Xb,Xp1) != Xp
& reflect(Xa,Xb,Xp) = Xp1
& Xa != Xb ),
inference(pre_NNF_transformation,[status(thm)],[f187]) ).
fof(f533,plain,
( reflect(sK0_skl,sK1_skl,sK3_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)],[f532]) ).
fof(f534,plain,
sK0_skl != sK1_skl,
inference(cnf_transformation,[status(thm)],[f533]) ).
fof(f535,plain,
reflect(sK0_skl,sK1_skl,sK2_skl) = sK3_skl,
inference(cnf_transformation,[status(thm)],[f533]) ).
fof(f536,plain,
reflect(sK0_skl,sK1_skl,sK3_skl) != sK2_skl,
inference(cnf_transformation,[status(thm)],[f533]) ).
fof(f665,definition,
( sQ6_spl
<=> sK0_skl = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f666,plain,
( ~ sQ6_spl
| sK0_skl = sK1_skl ),
inference(component_clause,[status(thm)],[f665]) ).
fof(f668,definition,
( sQ7_spl
<=> sK2_skl = reflect(sK0_skl,sK1_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f669,plain,
( ~ sQ7_spl
| sK2_skl = reflect(sK0_skl,sK1_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f668]) ).
fof(f675,plain,
( ~ sQ7_spl
| sK2_skl = sK3_skl ),
inference(forward_demodulation,[status(thm)],[f535,f669]) ).
fof(f676,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f666,f534]) ).
fof(f677,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f676]) ).
fof(f678,plain,
( ~ sQ7_spl
| reflect(sK0_skl,sK1_skl,sK3_skl) != sK3_skl ),
inference(backward_demodulation,[status(thm)],[f675,f536]) ).
fof(f679,plain,
( ~ sQ7_spl
| reflect(sK0_skl,sK1_skl,sK3_skl) = sK3_skl ),
inference(backward_demodulation,[status(thm)],[f675,f535]) ).
fof(f681,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f679,f678]) ).
fof(f682,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f681]) ).
fof(f778,plain,
! [X0,X1] : s_m(X0,midpoint(X1,X0),X1),
inference(resolution,[status(thm)],[f360,f458]) ).
fof(f785,plain,
! [X0,X1] : X0 = s(midpoint(X0,X1),X1),
inference(resolution,[status(thm)],[f366,f778]) ).
fof(f786,plain,
! [X0,X1] : X0 = s(midpoint(X1,X0),X1),
inference(resolution,[status(thm)],[f366,f458]) ).
fof(f829,plain,
! [X0,X1] : X0 = midpoint(X1,s(X0,X1)),
inference(resolution,[status(thm)],[f386,f786]) ).
fof(f847,plain,
! [X0,X1] : midpoint(X0,X1) = midpoint(X1,X0),
inference(paramodulation,[status(thm)],[f785,f829]) ).
fof(f7551,plain,
! [X0,X1,X2] :
( X2 = reflect(X0,X1,X2)
| X0 = X1
| perp(X0,X1,reflect(X0,X1,X2),X2) ),
inference(resolution,[status(thm)],[f473,f528]) ).
fof(f7644,plain,
( sK2_skl = reflect(sK0_skl,sK1_skl,sK2_skl)
| sK0_skl = sK1_skl
| perp(sK0_skl,sK1_skl,sK3_skl,sK2_skl) ),
inference(paramodulation,[status(thm)],[f535,f7551]) ).
fof(f7648,definition,
( sQ168_spl
<=> perp(sK0_skl,sK1_skl,sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f7651,plain,
( sQ7_spl
| sQ6_spl
| sQ168_spl ),
inference(split_clause,[status(thm)],[f7644,f7648,f665,f668]) ).
fof(f10977,plain,
( s_col(sK0_skl,sK1_skl,midpoint(sK2_skl,sK3_skl))
| sK0_skl = sK1_skl ),
inference(paramodulation,[status(thm)],[f535,f527]) ).
fof(f11003,definition,
( sQ429_spl
<=> s_col(sK0_skl,sK1_skl,midpoint(sK2_skl,sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ429_spl])],[split_symbol_definition]) ).
fof(f11004,plain,
( ~ sQ429_spl
| s_col(sK0_skl,sK1_skl,midpoint(sK2_skl,sK3_skl)) ),
inference(component_clause,[status(thm)],[f11003]) ).
fof(f11006,plain,
( sQ429_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f10977,f665,f11003]) ).
fof(f11947,plain,
( ~ sQ429_spl
| s_col(sK0_skl,sK1_skl,midpoint(sK3_skl,sK2_skl)) ),
inference(paramodulation,[status(thm)],[f847,f11004]) ).
fof(f19906,plain,
( ~ sQ429_spl
| sK2_skl = reflect(sK0_skl,sK1_skl,sK3_skl)
| ~ perp(sK0_skl,sK1_skl,sK3_skl,sK2_skl)
| sK0_skl = sK1_skl ),
inference(resolution,[status(thm)],[f11947,f530]) ).
fof(f19919,definition,
( sQ1011_spl
<=> sK2_skl = reflect(sK0_skl,sK1_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ1011_spl])],[split_symbol_definition]) ).
fof(f19920,plain,
( ~ sQ1011_spl
| sK2_skl = reflect(sK0_skl,sK1_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f19919]) ).
fof(f19922,plain,
( ~ sQ429_spl
| sQ1011_spl
| ~ sQ168_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f19906,f665,f7648,f19919,f11003]) ).
fof(f19954,plain,
( ~ sQ1011_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19920,f536]) ).
fof(f19955,plain,
~ sQ1011_spl,
inference(contradiction_clause,[status(thm)],[f19954]) ).
fof(f19956,plain,
$false,
inference(sat_refutation,[status(thm)],[f677,f682,f7651,f11006,f19922,f19955]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO523+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.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 17:14:12 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 60.48/8.08 % Refutation found
% 60.48/8.08 % SZS status Theorem for theBenchmark: Theorem is valid
% 60.48/8.08 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.65/8.11 % Elapsed time: 7.742983 seconds
% 3.65/8.11 % CPU time: 61.027210 seconds
% 3.65/8.11 % Total memory used: 266.462 MB
% 3.65/8.11 % Net memory used: 237.973 MB
%------------------------------------------------------------------------------