%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SEU261+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 02:19:56 PM UTC 2026
% Result : Theorem 57.83s 7.79s
% Output : CNFRefutation 3.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 19
% Syntax : Number of formulae : 84 ( 14 unt; 16 def)
% Number of atoms : 304 ( 0 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 366 ( 146 ~; 146 |; 38 &)
% ( 18 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 26 ( 25 usr; 17 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 39 ( 36 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f51,axiom,
! [A] :
( relation(A)
=> ( well_ordering(A)
<=> ( well_founded_relation(A)
& connected(A)
& antisymmetric(A)
& transitive(A)
& reflexive(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f280,lemma,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( relation_isomorphism(A,B,C)
=> ( ( well_founded_relation(A)
=> well_founded_relation(B) )
& ( antisymmetric(A)
=> antisymmetric(B) )
& ( connected(A)
=> connected(B) )
& ( transitive(A)
=> transitive(B) )
& ( reflexive(A)
=> reflexive(B) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f283,conjecture,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( ( relation_isomorphism(A,B,C)
& well_ordering(A) )
=> well_ordering(B) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f284,negated_conjecture,
~ ! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ! [C] :
( ( function(C)
& relation(C) )
=> ( ( relation_isomorphism(A,B,C)
& well_ordering(A) )
=> well_ordering(B) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f283]) ).
fof(f640,plain,
! [A] :
( ( well_ordering(A)
<=> ( well_founded_relation(A)
& connected(A)
& antisymmetric(A)
& transitive(A)
& reflexive(A) ) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f641,plain,
! [A] :
( ( ( ~ well_founded_relation(A)
| ~ connected(A)
| ~ antisymmetric(A)
| ~ transitive(A)
| ~ reflexive(A)
| well_ordering(A) )
& ( ( well_founded_relation(A)
& connected(A)
& antisymmetric(A)
& transitive(A)
& reflexive(A) )
| ~ well_ordering(A) ) )
| ~ relation(A) ),
inference(NNF_transformation,[status(thm)],[f640]) ).
fof(f642,plain,
! [X0] :
( reflexive(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f641]) ).
fof(f643,plain,
! [X0] :
( transitive(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f641]) ).
fof(f644,plain,
! [X0] :
( antisymmetric(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f641]) ).
fof(f645,plain,
! [X0] :
( connected(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f641]) ).
fof(f646,plain,
! [X0] :
( well_founded_relation(X0)
| ~ well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f641]) ).
fof(f647,plain,
! [X0] :
( ~ well_founded_relation(X0)
| ~ connected(X0)
| ~ antisymmetric(X0)
| ~ transitive(X0)
| ~ reflexive(X0)
| well_ordering(X0)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f641]) ).
fof(f1353,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( well_founded_relation(B)
| ~ well_founded_relation(A) )
& ( antisymmetric(B)
| ~ antisymmetric(A) )
& ( connected(B)
| ~ connected(A) )
& ( transitive(B)
| ~ transitive(A) )
& ( reflexive(B)
| ~ reflexive(A) ) )
| ~ relation_isomorphism(A,B,C)
| ~ function(C)
| ~ relation(C) )
| ~ relation(B) )
| ~ relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f280]) ).
fof(f1354,plain,
! [X0,X1,X2] :
( reflexive(X1)
| ~ reflexive(X0)
| ~ relation_isomorphism(X0,X1,X2)
| ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1353]) ).
fof(f1355,plain,
! [X0,X1,X2] :
( transitive(X1)
| ~ transitive(X0)
| ~ relation_isomorphism(X0,X1,X2)
| ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1353]) ).
fof(f1356,plain,
! [X0,X1,X2] :
( connected(X1)
| ~ connected(X0)
| ~ relation_isomorphism(X0,X1,X2)
| ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1353]) ).
fof(f1357,plain,
! [X0,X1,X2] :
( antisymmetric(X1)
| ~ antisymmetric(X0)
| ~ relation_isomorphism(X0,X1,X2)
| ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1353]) ).
fof(f1358,plain,
! [X0,X1,X2] :
( well_founded_relation(X1)
| ~ well_founded_relation(X0)
| ~ relation_isomorphism(X0,X1,X2)
| ~ function(X2)
| ~ relation(X2)
| ~ relation(X1)
| ~ relation(X0) ),
inference(cnf_transformation,[status(thm)],[f1353]) ).
fof(f1375,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ well_ordering(B)
& relation_isomorphism(A,B,C)
& well_ordering(A)
& function(C)
& relation(C) )
& relation(B) )
& relation(A) ),
inference(pre_NNF_transformation,[status(thm)],[f284]) ).
fof(f1376,plain,
( ~ well_ordering(sK119_skl)
& relation_isomorphism(sK118_skl,sK119_skl,sK120_skl)
& well_ordering(sK118_skl)
& function(sK120_skl)
& relation(sK120_skl)
& relation(sK119_skl)
& relation(sK118_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK118_skl,sK119_skl,sK120_skl]),skolemize(A,sK118_skl),skolemize(B,sK119_skl),skolemize(C,sK120_skl)],[f1375]) ).
fof(f1377,plain,
relation(sK118_skl),
inference(cnf_transformation,[status(thm)],[f1376]) ).
fof(f1378,plain,
relation(sK119_skl),
inference(cnf_transformation,[status(thm)],[f1376]) ).
fof(f1379,plain,
relation(sK120_skl),
inference(cnf_transformation,[status(thm)],[f1376]) ).
fof(f1380,plain,
function(sK120_skl),
inference(cnf_transformation,[status(thm)],[f1376]) ).
fof(f1381,plain,
well_ordering(sK118_skl),
inference(cnf_transformation,[status(thm)],[f1376]) ).
fof(f1382,plain,
relation_isomorphism(sK118_skl,sK119_skl,sK120_skl),
inference(cnf_transformation,[status(thm)],[f1376]) ).
fof(f1383,plain,
~ well_ordering(sK119_skl),
inference(cnf_transformation,[status(thm)],[f1376]) ).
fof(f1648,plain,
( connected(sK118_skl)
| ~ well_ordering(sK118_skl) ),
inference(resolution,[status(thm)],[f645,f1377]) ).
fof(f1656,definition,
( sQ4_spl
<=> well_ordering(sK119_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1657,plain,
( ~ sQ4_spl
| well_ordering(sK119_skl) ),
inference(component_clause,[status(thm)],[f1656]) ).
fof(f1659,definition,
( sQ5_spl
<=> connected(sK119_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1663,definition,
( sQ6_spl
<=> well_ordering(sK118_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1665,plain,
( sQ6_spl
| ~ well_ordering(sK118_skl) ),
inference(component_clause,[status(thm)],[f1663]) ).
fof(f1666,definition,
( sQ7_spl
<=> connected(sK118_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1669,plain,
( sQ7_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1648,f1663,f1666]) ).
fof(f1672,plain,
( well_founded_relation(sK118_skl)
| ~ well_ordering(sK118_skl) ),
inference(resolution,[status(thm)],[f646,f1377]) ).
fof(f1677,definition,
( sQ9_spl
<=> well_founded_relation(sK119_skl) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f1681,definition,
( sQ10_spl
<=> well_founded_relation(sK118_skl) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f1684,plain,
( sQ10_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f1672,f1663,f1681]) ).
fof(f1685,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1665,f1381]) ).
fof(f1686,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f1685]) ).
fof(f1688,definition,
( sQ11_spl
<=> relation(sK118_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1690,plain,
( sQ11_spl
| ~ relation(sK118_skl) ),
inference(component_clause,[status(thm)],[f1688]) ).
fof(f1691,definition,
( sQ12_spl
<=> relation(sK119_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f1693,plain,
( sQ12_spl
| ~ relation(sK119_skl) ),
inference(component_clause,[status(thm)],[f1691]) ).
fof(f1694,definition,
( sQ13_spl
<=> relation(sK120_skl) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f1696,plain,
( sQ13_spl
| ~ relation(sK120_skl) ),
inference(component_clause,[status(thm)],[f1694]) ).
fof(f1697,definition,
( sQ14_spl
<=> function(sK120_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f1699,plain,
( sQ14_spl
| ~ function(sK120_skl) ),
inference(component_clause,[status(thm)],[f1697]) ).
fof(f1709,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1699,f1380]) ).
fof(f1710,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f1709]) ).
fof(f1711,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1696,f1379]) ).
fof(f1712,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f1711]) ).
fof(f1713,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1693,f1378]) ).
fof(f1714,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f1713]) ).
fof(f1715,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1690,f1377]) ).
fof(f1716,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f1715]) ).
fof(f2425,definition,
( sQ137_spl
<=> antisymmetric(sK119_skl) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f2432,definition,
( sQ139_spl
<=> antisymmetric(sK118_skl) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f3386,definition,
( sQ283_spl
<=> transitive(sK119_skl) ),
introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition]) ).
fof(f3393,definition,
( sQ285_spl
<=> transitive(sK118_skl) ),
introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition]) ).
fof(f7806,plain,
( reflexive(sK118_skl)
| ~ well_ordering(sK118_skl) ),
inference(resolution,[status(thm)],[f642,f1377]) ).
fof(f7815,definition,
( sQ574_spl
<=> reflexive(sK119_skl) ),
introduced(definition,[new_symbols(definition,[sQ574_spl])],[split_symbol_definition]) ).
fof(f7855,definition,
( sQ584_spl
<=> reflexive(sK118_skl) ),
introduced(definition,[new_symbols(definition,[sQ584_spl])],[split_symbol_definition]) ).
fof(f7858,plain,
( sQ584_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f7806,f1663,f7855]) ).
fof(f7871,plain,
( transitive(sK118_skl)
| ~ well_ordering(sK118_skl) ),
inference(resolution,[status(thm)],[f643,f1377]) ).
fof(f7884,plain,
( sQ285_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f7871,f1663,f3393]) ).
fof(f7897,plain,
( antisymmetric(sK118_skl)
| ~ well_ordering(sK118_skl) ),
inference(resolution,[status(thm)],[f644,f1377]) ).
fof(f7910,plain,
( sQ139_spl
| ~ sQ6_spl ),
inference(split_clause,[status(thm)],[f7897,f1663,f2432]) ).
fof(f7913,plain,
( ~ well_founded_relation(sK119_skl)
| ~ connected(sK119_skl)
| ~ antisymmetric(sK119_skl)
| ~ transitive(sK119_skl)
| ~ reflexive(sK119_skl)
| well_ordering(sK119_skl) ),
inference(resolution,[status(thm)],[f647,f1378]) ).
fof(f7926,plain,
( ~ sQ9_spl
| ~ sQ5_spl
| ~ sQ137_spl
| ~ sQ283_spl
| ~ sQ574_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f7913,f1656,f7815,f3386,f2425,f1659,f1677]) ).
fof(f32972,plain,
( reflexive(sK119_skl)
| ~ reflexive(sK118_skl)
| ~ function(sK120_skl)
| ~ relation(sK120_skl)
| ~ relation(sK119_skl)
| ~ relation(sK118_skl) ),
inference(resolution,[status(thm)],[f1354,f1382]) ).
fof(f32973,plain,
( sQ574_spl
| ~ sQ584_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f32972,f1688,f1691,f1694,f1697,f7855,f7815]) ).
fof(f32974,plain,
( transitive(sK119_skl)
| ~ transitive(sK118_skl)
| ~ function(sK120_skl)
| ~ relation(sK120_skl)
| ~ relation(sK119_skl)
| ~ relation(sK118_skl) ),
inference(resolution,[status(thm)],[f1355,f1382]) ).
fof(f32975,plain,
( sQ283_spl
| ~ sQ285_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f32974,f1688,f1691,f1694,f1697,f3393,f3386]) ).
fof(f32976,plain,
( connected(sK119_skl)
| ~ connected(sK118_skl)
| ~ function(sK120_skl)
| ~ relation(sK120_skl)
| ~ relation(sK119_skl)
| ~ relation(sK118_skl) ),
inference(resolution,[status(thm)],[f1356,f1382]) ).
fof(f32977,plain,
( sQ5_spl
| ~ sQ7_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f32976,f1688,f1691,f1694,f1697,f1666,f1659]) ).
fof(f32978,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1657,f1383]) ).
fof(f32979,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f32978]) ).
fof(f33038,plain,
( antisymmetric(sK119_skl)
| ~ antisymmetric(sK118_skl)
| ~ function(sK120_skl)
| ~ relation(sK120_skl)
| ~ relation(sK119_skl)
| ~ relation(sK118_skl) ),
inference(resolution,[status(thm)],[f1357,f1382]) ).
fof(f33039,plain,
( sQ137_spl
| ~ sQ139_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f33038,f1688,f1691,f1694,f1697,f2432,f2425]) ).
fof(f33040,plain,
( well_founded_relation(sK119_skl)
| ~ well_founded_relation(sK118_skl)
| ~ function(sK120_skl)
| ~ relation(sK120_skl)
| ~ relation(sK119_skl)
| ~ relation(sK118_skl) ),
inference(resolution,[status(thm)],[f1358,f1382]) ).
fof(f33041,plain,
( sQ9_spl
| ~ sQ10_spl
| ~ sQ14_spl
| ~ sQ13_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f33040,f1688,f1691,f1694,f1697,f1681,f1677]) ).
fof(f33042,plain,
$false,
inference(sat_refutation,[status(thm)],[f1669,f1684,f1686,f1710,f1712,f1714,f1716,f7858,f7884,f7910,f7926,f32973,f32975,f32977,f32979,f33039,f33041]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU261+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 06:09:37 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 57.83/7.79 % Refutation found
% 57.83/7.79 % SZS status Theorem for theBenchmark: Theorem is valid
% 57.83/7.79 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.96/7.98 % Elapsed time: 7.610289 seconds
% 3.96/7.98 % CPU time: 59.001901 seconds
% 3.96/7.98 % Total memory used: 474.923 MB
% 3.96/7.98 % Net memory used: 425.269 MB
%------------------------------------------------------------------------------