%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO507+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:09 PM UTC 2026
% Result : Theorem 146.01s 19.09s
% Output : CNFRefutation 146.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 13
% Syntax : Number of formulae : 63 ( 17 unt; 5 def)
% Number of atoms : 198 ( 30 equ)
% Maximal formula atoms : 30 ( 3 avg)
% Number of connectives : 224 ( 89 ~; 102 |; 28 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 6 prp; 0-5 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-5 aty)
% Number of variables : 154 ( 146 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f22,axiom,
! [Xa1,Xb1] : s_t(Xa1,Xa1,Xb1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [Xa,Xb] : s_col(Xa,Xb,Xa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f124,axiom,
! [Xa,Xb] :
( Xa = Xb
| ~ s_r(Xa,Xb,Xa) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,axiom,
! [Xa,Xb,Xc,Xp,Xq] :
( perpAt(Xp,Xq,Xc,Xa,Xb)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f131,conjecture,
! [Xa,Xb,Xp,Xq] :
( ~ s_col(Xa,Xb,Xq)
| ~ s_col(Xa,Xb,Xp)
| ~ perp(Xa,Xb,Xp,Xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,negated_conjecture,
~ ! [Xa,Xb,Xp,Xq] :
( ~ s_col(Xa,Xb,Xq)
| ~ s_col(Xa,Xb,Xp)
| ~ perp(Xa,Xb,Xp,Xq) ),
inference(negated_conjecture,[status(cth)],[f131]) ).
fof(f137,axiom,
! [Xa,Xb,Xc] :
( ( ~ s_t(Xc,Xa,Xb)
| s_col(Xa,Xb,Xc) )
& ( ~ s_t(Xb,Xc,Xa)
| s_col(Xa,Xb,Xc) )
& ( ~ s_t(Xa,Xb,Xc)
| s_col(Xa,Xb,Xc) )
& ( s_t(Xc,Xa,Xb)
| s_t(Xb,Xc,Xa)
| s_t(Xa,Xb,Xc)
| ~ s_col(Xa,Xb,Xc) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f144,axiom,
! [Y,Z,X,Y1,Z1,U,V] :
( ( ~ s_r(f811(Y,Z,Y1,Z1,X),X,g811(Y,Z,Y1,Z1,X))
| ~ s_col(Y1,Z1,X)
| ~ s_col(Y,Z,X)
| Y1 = Z1
| Y = Z
| perpAt(Y,Z,X,Y1,Z1) )
& ( s_col(Y1,Z1,g811(Y,Z,Y1,Z1,X))
| ~ s_col(Y1,Z1,X)
| ~ s_col(Y,Z,X)
| Y1 = Z1
| Y = Z
| perpAt(Y,Z,X,Y1,Z1) )
& ( s_col(Y,Z,f811(Y,Z,Y1,Z1,X))
| ~ s_col(Y1,Z1,X)
| ~ s_col(Y,Z,X)
| Y1 = Z1
| Y = Z
| perpAt(Y,Z,X,Y1,Z1) )
& ( s_r(U,X,V)
| ~ s_col(Y1,Z1,V)
| ~ s_col(Y,Z,U)
| ~ perpAt(Y,Z,X,Y1,Z1) )
& ( Y1 != Z1
| ~ perpAt(Y,Z,X,Y1,Z1) )
& ( Y != Z
| ~ perpAt(Y,Z,X,Y1,Z1) )
& ( s_col(Y1,Z1,X)
| ~ perpAt(Y,Z,X,Y1,Z1) )
& ( s_col(Y,Z,X)
| ~ perpAt(Y,Z,X,Y1,Z1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,axiom,
! [Xp,Xq,Xp1,Xq1,X] :
( ( ~ perpAt(Xp,Xq,X,Xp1,Xq1)
| perp(Xp,Xq,Xp1,Xq1) )
& ( perpAt(Xp,Xq,il(Xp,Xq,Xp1,Xq1),Xp1,Xq1)
| ~ perp(Xp,Xq,Xp1,Xq1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f180,plain,
! [X0,X1] : s_t(X0,X0,X1),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f218,plain,
! [X0,X1] : s_col(X0,X1,X0),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f351,plain,
! [X0,X1] :
( ~ s_r(X1,X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f356,plain,
! [X0,X1,X2,X3,X4] :
( ~ perpAt(X3,X4,X2,X0,X1)
| perpAt(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f370,plain,
? [Xa,Xb,Xp,Xq] :
( s_col(Xa,Xb,Xq)
& s_col(Xa,Xb,Xp)
& perp(Xa,Xb,Xp,Xq) ),
inference(pre_NNF_transformation,[status(thm)],[f132]) ).
fof(f371,plain,
? [Xa,Xb,Xq] :
( s_col(Xa,Xb,Xq)
& ? [Xp] :
( s_col(Xa,Xb,Xp)
& perp(Xa,Xb,Xp,Xq) ) ),
inference(miniscoping,[status(thm)],[f370]) ).
fof(f372,plain,
( s_col(sK0_skl,sK1_skl,sK2_skl)
& s_col(sK0_skl,sK1_skl,sK3_skl)
& perp(sK0_skl,sK1_skl,sK3_skl,sK2_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(Xq,sK2_skl),skolemize(Xp,sK3_skl)],[f371]) ).
fof(f373,plain,
perp(sK0_skl,sK1_skl,sK3_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f374,plain,
s_col(sK0_skl,sK1_skl,sK3_skl),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f375,plain,
s_col(sK0_skl,sK1_skl,sK2_skl),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f398,plain,
( ! [Xa,Xb,Xc] :
( ~ s_t(Xc,Xa,Xb)
| s_col(Xa,Xb,Xc) )
& ! [Xa,Xb,Xc] :
( ~ s_t(Xb,Xc,Xa)
| s_col(Xa,Xb,Xc) )
& ! [Xa,Xb,Xc] :
( ~ s_t(Xa,Xb,Xc)
| s_col(Xa,Xb,Xc) )
& ! [Xa,Xb,Xc] :
( s_t(Xc,Xa,Xb)
| s_t(Xb,Xc,Xa)
| s_t(Xa,Xb,Xc)
| ~ s_col(Xa,Xb,Xc) ) ),
inference(miniscoping,[status(thm)],[f137]) ).
fof(f401,plain,
! [X0,X1,X2] :
( ~ s_t(X1,X2,X0)
| s_col(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f398]) ).
fof(f434,plain,
( ! [Y,Z,X,Y1,Z1] :
( ~ s_r(f811(Y,Z,Y1,Z1,X),X,g811(Y,Z,Y1,Z1,X))
| ~ s_col(Y1,Z1,X)
| ~ s_col(Y,Z,X)
| Y1 = Z1
| Y = Z
| perpAt(Y,Z,X,Y1,Z1) )
& ! [Y,Z,X,Y1,Z1] :
( s_col(Y1,Z1,g811(Y,Z,Y1,Z1,X))
| ~ s_col(Y1,Z1,X)
| ~ s_col(Y,Z,X)
| Y1 = Z1
| Y = Z
| perpAt(Y,Z,X,Y1,Z1) )
& ! [Y,Z,X,Y1,Z1] :
( s_col(Y,Z,f811(Y,Z,Y1,Z1,X))
| ~ s_col(Y1,Z1,X)
| ~ s_col(Y,Z,X)
| Y1 = Z1
| Y = Z
| perpAt(Y,Z,X,Y1,Z1) )
& ! [X,U,V] :
( s_r(U,X,V)
| ! [Y1,Z1] :
( ~ s_col(Y1,Z1,V)
| ! [Y,Z] :
( ~ s_col(Y,Z,U)
| ~ perpAt(Y,Z,X,Y1,Z1) ) ) )
& ! [Y1,Z1] :
( Y1 != Z1
| ! [Y,Z,X] : ~ perpAt(Y,Z,X,Y1,Z1) )
& ! [Y,Z] :
( Y != Z
| ! [X,Y1,Z1] : ~ perpAt(Y,Z,X,Y1,Z1) )
& ! [X,Y1,Z1] :
( s_col(Y1,Z1,X)
| ! [Y,Z] : ~ perpAt(Y,Z,X,Y1,Z1) )
& ! [Y,Z,X] :
( s_col(Y,Z,X)
| ! [Y1,Z1] : ~ perpAt(Y,Z,X,Y1,Z1) ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f438,plain,
! [X0,X1,X2,X3,X4] :
( X3 != X4
| ~ perpAt(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f434]) ).
fof(f439,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( s_r(X5,X6,X2)
| ~ perpAt(X3,X4,X6,X0,X1)
| ~ s_col(X3,X4,X5)
| ~ s_col(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f434]) ).
fof(f443,plain,
( ! [Xp,Xq,Xp1,Xq1] :
( ! [X] : ~ perpAt(Xp,Xq,X,Xp1,Xq1)
| perp(Xp,Xq,Xp1,Xq1) )
& ! [Xp,Xq,Xp1,Xq1] :
( perpAt(Xp,Xq,il(Xp,Xq,Xp1,Xq1),Xp1,Xq1)
| ~ perp(Xp,Xq,Xp1,Xq1) ) ),
inference(miniscoping,[status(thm)],[f145]) ).
fof(f444,plain,
! [X0,X1,X2,X3] :
( ~ perp(X0,X1,X2,X3)
| perpAt(X0,X1,il(X0,X1,X2,X3),X2,X3) ),
inference(cnf_transformation,[status(thm)],[f443]) ).
fof(f445,plain,
! [X0,X1,X2,X3,X4] :
( perp(X0,X1,X3,X4)
| ~ perpAt(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(thm)],[f443]) ).
fof(f447,plain,
! [X0,X1,X2,X3] : ~ perpAt(X0,X1,X2,X3,X3),
inference(destructive_equality_resolution,[status(thm)],[f438]) ).
fof(f462,plain,
! [X0,X1] : s_col(X0,X1,X1),
inference(resolution,[status(thm)],[f180,f401]) ).
fof(f1305,plain,
perpAt(sK0_skl,sK1_skl,il(sK0_skl,sK1_skl,sK3_skl,sK2_skl),sK3_skl,sK2_skl),
inference(resolution,[status(thm)],[f444,f373]) ).
fof(f1307,plain,
! [X0,X1,X2,X3,X4] :
( perpAt(X0,X1,il(X0,X1,X3,X4),X3,X4)
| ~ perpAt(X0,X1,X2,X3,X4) ),
inference(resolution,[status(thm)],[f444,f445]) ).
fof(f1460,plain,
perpAt(sK3_skl,sK2_skl,il(sK0_skl,sK1_skl,sK3_skl,sK2_skl),sK0_skl,sK1_skl),
inference(resolution,[status(thm)],[f356,f1305]) ).
fof(f1556,plain,
perpAt(sK3_skl,sK2_skl,il(sK3_skl,sK2_skl,sK0_skl,sK1_skl),sK0_skl,sK1_skl),
inference(resolution,[status(thm)],[f1307,f1460]) ).
fof(f1595,plain,
perpAt(sK0_skl,sK1_skl,il(sK3_skl,sK2_skl,sK0_skl,sK1_skl),sK3_skl,sK2_skl),
inference(resolution,[status(thm)],[f1556,f356]) ).
fof(f1919,plain,
! [X0,X1] :
( s_r(X0,il(sK3_skl,sK2_skl,sK0_skl,sK1_skl),X1)
| ~ s_col(sK3_skl,sK2_skl,X1)
| ~ s_col(sK0_skl,sK1_skl,X0) ),
inference(resolution,[status(thm)],[f439,f1595]) ).
fof(f2013,plain,
! [X0] :
( ~ s_col(sK3_skl,sK2_skl,X0)
| X0 = il(sK3_skl,sK2_skl,sK0_skl,sK1_skl)
| ~ s_col(sK0_skl,sK1_skl,X0) ),
inference(resolution,[status(thm)],[f1919,f351]) ).
fof(f2309,plain,
( il(sK3_skl,sK2_skl,sK0_skl,sK1_skl) = sK2_skl
| ~ s_col(sK0_skl,sK1_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f2013,f462]) ).
fof(f2316,plain,
( il(sK3_skl,sK2_skl,sK0_skl,sK1_skl) = sK3_skl
| ~ s_col(sK0_skl,sK1_skl,sK3_skl) ),
inference(resolution,[status(thm)],[f2013,f218]) ).
fof(f2323,definition,
( sQ64_spl
<=> sK2_skl = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f2324,plain,
( ~ sQ64_spl
| sK3_skl = sK2_skl ),
inference(component_clause,[status(thm)],[f2323]) ).
fof(f2325,plain,
( sQ64_spl
| sK2_skl != sK3_skl ),
inference(component_clause,[status(thm)],[f2323]) ).
fof(f2331,definition,
( sQ66_spl
<=> s_col(sK0_skl,sK1_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f2333,plain,
( sQ66_spl
| ~ s_col(sK0_skl,sK1_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f2331]) ).
fof(f2334,definition,
( sQ67_spl
<=> il(sK3_skl,sK2_skl,sK0_skl,sK1_skl) = sK3_skl ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f2335,plain,
( ~ sQ67_spl
| sK3_skl = il(sK3_skl,sK2_skl,sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f2334]) ).
fof(f2337,plain,
( sQ67_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f2316,f2331,f2334]) ).
fof(f2374,definition,
( sQ78_spl
<=> s_col(sK0_skl,sK1_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f2376,plain,
( sQ78_spl
| ~ s_col(sK0_skl,sK1_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f2374]) ).
fof(f2377,definition,
( sQ79_spl
<=> il(sK3_skl,sK2_skl,sK0_skl,sK1_skl) = sK2_skl ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f2378,plain,
( ~ sQ79_spl
| sK2_skl = il(sK3_skl,sK2_skl,sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f2377]) ).
fof(f2380,plain,
( sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f2309,f2374,f2377]) ).
fof(f2404,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2333,f374]) ).
fof(f2405,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f2404]) ).
fof(f2408,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2376,f375]) ).
fof(f2409,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f2408]) ).
fof(f2433,plain,
( ~ sQ64_spl
| perpAt(sK0_skl,sK1_skl,il(sK0_skl,sK1_skl,sK3_skl,sK2_skl),sK2_skl,sK2_skl) ),
inference(backward_demodulation,[status(thm)],[f2324,f1305]) ).
fof(f2436,plain,
( ~ sQ64_spl
| perpAt(sK0_skl,sK1_skl,il(sK0_skl,sK1_skl,sK2_skl,sK2_skl),sK2_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f2324,f2433]) ).
fof(f2437,plain,
( ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2436,f447]) ).
fof(f2438,plain,
~ sQ64_spl,
inference(contradiction_clause,[status(thm)],[f2437]) ).
fof(f2931,plain,
( ~ sQ79_spl
| ~ sQ67_spl
| sK2_skl = sK3_skl ),
inference(forward_demodulation,[status(thm)],[f2335,f2378]) ).
fof(f2932,plain,
( ~ sQ79_spl
| ~ sQ67_spl
| sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2931,f2325]) ).
fof(f2933,plain,
( ~ sQ79_spl
| ~ sQ67_spl
| sQ64_spl ),
inference(contradiction_clause,[status(thm)],[f2932]) ).
fof(f2934,plain,
$false,
inference(sat_refutation,[status(thm)],[f2337,f2380,f2405,f2409,f2438,f2933]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO507+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.57 % Computer : n005.cluster.edu
% 0.09/0.57 % Model : x86_64 x86_64
% 0.09/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.57 % Memory : 8046.5625MB
% 0.09/0.57 % OS : Linux 6.8.0-71-generic
% 0.09/0.57 % CPULimit : 300
% 0.09/0.57 % WCLimit : 300
% 0.09/0.57 % DateTime : Sun Sep 20 17:02:03 UTC 2026
% 0.09/0.57 % CPUTime :
% 0.13/0.58 % Drodi V4.1.1
% 146.01/19.09 % Refutation found
% 146.01/19.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 146.01/19.09 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 33.63/19.13 % Elapsed time: 18.538446 seconds
% 33.63/19.13 % CPU time: 146.899543 seconds
% 33.63/19.13 % Total memory used: 245.296 MB
% 33.63/19.13 % Net memory used: 210.920 MB
%------------------------------------------------------------------------------