%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : RNG111+1 : TPTP v9.3.1. Released v4.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 02:05:00 PM UTC 2026
% Result : Theorem 0.13s 0.38s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 8
% Syntax : Number of formulae : 45 ( 5 unt; 7 def)
% Number of atoms : 184 ( 57 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 228 ( 89 ~; 90 |; 30 &)
% ( 7 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 8 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-1 aty)
% Number of variables : 31 ( 24 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f45,conjecture,
! [W0] :
( ( W0 != sz00
& aElementOf0(W0,xI) )
=> ( ! [W1] :
( ( W1 != sz00
& aElementOf0(W1,xI) )
=> ( iLess0(sbrdtbr0(W1),sbrdtbr0(W0))
=> ? [W2] :
( ! [W3] :
( ( W3 != sz00
& aElementOf0(W3,xI) )
=> ~ iLess0(sbrdtbr0(W3),sbrdtbr0(W2)) )
& W2 != sz00
& aElementOf0(W2,xI) ) ) )
=> ? [W1] :
( ! [W2] :
( ( W2 != sz00
& aElementOf0(W2,xI) )
=> ~ iLess0(sbrdtbr0(W2),sbrdtbr0(W1)) )
& W1 != sz00
& aElementOf0(W1,xI) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
~ ! [W0] :
( ( W0 != sz00
& aElementOf0(W0,xI) )
=> ( ! [W1] :
( ( W1 != sz00
& aElementOf0(W1,xI) )
=> ( iLess0(sbrdtbr0(W1),sbrdtbr0(W0))
=> ? [W2] :
( ! [W3] :
( ( W3 != sz00
& aElementOf0(W3,xI) )
=> ~ iLess0(sbrdtbr0(W3),sbrdtbr0(W2)) )
& W2 != sz00
& aElementOf0(W2,xI) ) ) )
=> ? [W1] :
( ! [W2] :
( ( W2 != sz00
& aElementOf0(W2,xI) )
=> ~ iLess0(sbrdtbr0(W2),sbrdtbr0(W1)) )
& W1 != sz00
& aElementOf0(W1,xI) ) ) ),
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f212,plain,
? [W0] :
( ! [W1] :
( ? [W2] :
( iLess0(sbrdtbr0(W2),sbrdtbr0(W1))
& W2 != sz00
& aElementOf0(W2,xI) )
| W1 = sz00
| ~ aElementOf0(W1,xI) )
& ! [W1] :
( ? [W2] :
( ! [W3] :
( ~ iLess0(sbrdtbr0(W3),sbrdtbr0(W2))
| W3 = sz00
| ~ aElementOf0(W3,xI) )
& W2 != sz00
& aElementOf0(W2,xI) )
| ~ iLess0(sbrdtbr0(W1),sbrdtbr0(W0))
| W1 = sz00
| ~ aElementOf0(W1,xI) )
& W0 != sz00
& aElementOf0(W0,xI) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f213,plain,
( ! [W1] :
( ( iLess0(sbrdtbr0(sK23_skl(W1)),sbrdtbr0(W1))
& sK23_skl(W1) != sz00
& aElementOf0(sK23_skl(W1),xI) )
| W1 = sz00
| ~ aElementOf0(W1,xI) )
& ! [W1] :
( ( ! [W3] :
( ~ iLess0(sbrdtbr0(W3),sbrdtbr0(sK22_skl(W1)))
| W3 = sz00
| ~ aElementOf0(W3,xI) )
& sK22_skl(W1) != sz00
& aElementOf0(sK22_skl(W1),xI) )
| ~ iLess0(sbrdtbr0(W1),sbrdtbr0(sK21_skl))
| W1 = sz00
| ~ aElementOf0(W1,xI) )
& sK21_skl != sz00
& aElementOf0(sK21_skl,xI) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl,sK23_skl]),skolemize(W0,sK21_skl),skolemize(W2,sK22_skl(W1)),skolemize(W2,sK23_skl(W1))],[f212]) ).
fof(f214,plain,
aElementOf0(sK21_skl,xI),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f215,plain,
sK21_skl != sz00,
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f216,plain,
! [X0] :
( aElementOf0(sK22_skl(X0),xI)
| ~ iLess0(sbrdtbr0(X0),sbrdtbr0(sK21_skl))
| X0 = sz00
| ~ aElementOf0(X0,xI) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f217,plain,
! [X0] :
( sK22_skl(X0) != sz00
| ~ iLess0(sbrdtbr0(X0),sbrdtbr0(sK21_skl))
| X0 = sz00
| ~ aElementOf0(X0,xI) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f218,plain,
! [X0,X1] :
( ~ iLess0(sbrdtbr0(X1),sbrdtbr0(sK22_skl(X0)))
| X1 = sz00
| ~ aElementOf0(X1,xI)
| ~ iLess0(sbrdtbr0(X0),sbrdtbr0(sK21_skl))
| X0 = sz00
| ~ aElementOf0(X0,xI) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f219,plain,
! [X0] :
( aElementOf0(sK23_skl(X0),xI)
| X0 = sz00
| ~ aElementOf0(X0,xI) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f220,plain,
! [X0] :
( sK23_skl(X0) != sz00
| X0 = sz00
| ~ aElementOf0(X0,xI) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f221,plain,
! [X0] :
( iLess0(sbrdtbr0(sK23_skl(X0)),sbrdtbr0(X0))
| X0 = sz00
| ~ aElementOf0(X0,xI) ),
inference(cnf_transformation,[status(thm)],[f213]) ).
fof(f259,plain,
( sK21_skl = sz00
| ~ aElementOf0(sK21_skl,xI)
| aElementOf0(sK22_skl(sK23_skl(sK21_skl)),xI)
| sK23_skl(sK21_skl) = sz00
| ~ aElementOf0(sK23_skl(sK21_skl),xI) ),
inference(resolution,[status(thm)],[f216,f221]) ).
fof(f260,definition,
( sQ2_spl
<=> aElementOf0(sK23_skl(sK21_skl),xI) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f262,plain,
( sQ2_spl
| ~ aElementOf0(sK23_skl(sK21_skl),xI) ),
inference(component_clause,[status(thm)],[f260]) ).
fof(f263,definition,
( sQ3_spl
<=> sK23_skl(sK21_skl) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f264,plain,
( ~ sQ3_spl
| sK23_skl(sK21_skl) = sz00 ),
inference(component_clause,[status(thm)],[f263]) ).
fof(f266,definition,
( sQ4_spl
<=> aElementOf0(sK22_skl(sK23_skl(sK21_skl)),xI) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f269,definition,
( sQ5_spl
<=> aElementOf0(sK21_skl,xI) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f271,plain,
( sQ5_spl
| ~ aElementOf0(sK21_skl,xI) ),
inference(component_clause,[status(thm)],[f269]) ).
fof(f272,definition,
( sQ6_spl
<=> sK21_skl = sz00 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f273,plain,
( ~ sQ6_spl
| sK21_skl = sz00 ),
inference(component_clause,[status(thm)],[f272]) ).
fof(f275,plain,
( sQ6_spl
| ~ sQ5_spl
| sQ4_spl
| sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f259,f260,f263,f266,f269,f272]) ).
fof(f276,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f273,f215]) ).
fof(f277,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f276]) ).
fof(f278,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f271,f214]) ).
fof(f279,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f278]) ).
fof(f280,plain,
! [X0] :
( sK22_skl(X0) = sz00
| ~ aElementOf0(sK22_skl(X0),xI)
| sK23_skl(sK22_skl(X0)) = sz00
| ~ aElementOf0(sK23_skl(sK22_skl(X0)),xI)
| ~ iLess0(sbrdtbr0(X0),sbrdtbr0(sK21_skl))
| X0 = sz00
| ~ aElementOf0(X0,xI) ),
inference(resolution,[status(thm)],[f218,f221]) ).
fof(f281,plain,
! [X0] :
( sK22_skl(X0) = sz00
| ~ aElementOf0(sK22_skl(X0),xI)
| sK23_skl(sK22_skl(X0)) = sz00
| ~ iLess0(sbrdtbr0(X0),sbrdtbr0(sK21_skl))
| X0 = sz00
| ~ aElementOf0(X0,xI) ),
inference(forward_subsumption_resolution,[status(thm)],[f280,f219]) ).
fof(f282,plain,
! [X0] :
( sK22_skl(X0) = sz00
| ~ aElementOf0(sK22_skl(X0),xI)
| ~ iLess0(sbrdtbr0(X0),sbrdtbr0(sK21_skl))
| X0 = sz00
| ~ aElementOf0(X0,xI) ),
inference(forward_subsumption_resolution,[status(thm)],[f281,f220]) ).
fof(f283,plain,
( sK21_skl = sz00
| ~ aElementOf0(sK21_skl,xI)
| sK22_skl(sK23_skl(sK21_skl)) = sz00
| ~ aElementOf0(sK22_skl(sK23_skl(sK21_skl)),xI)
| sK23_skl(sK21_skl) = sz00
| ~ aElementOf0(sK23_skl(sK21_skl),xI) ),
inference(resolution,[status(thm)],[f282,f221]) ).
fof(f284,definition,
( sQ7_spl
<=> sK22_skl(sK23_skl(sK21_skl)) = sz00 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f285,plain,
( ~ sQ7_spl
| sK22_skl(sK23_skl(sK21_skl)) = sz00 ),
inference(component_clause,[status(thm)],[f284]) ).
fof(f287,plain,
( sQ6_spl
| ~ sQ5_spl
| sQ7_spl
| ~ sQ4_spl
| sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f283,f260,f263,f266,f284,f269,f272]) ).
fof(f288,plain,
( ~ sQ3_spl
| sK21_skl = sz00
| ~ aElementOf0(sK21_skl,xI) ),
inference(resolution,[status(thm)],[f264,f220]) ).
fof(f292,plain,
( ~ sQ3_spl
| sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f288,f269,f272,f263]) ).
fof(f305,plain,
( sQ2_spl
| sK21_skl = sz00
| ~ aElementOf0(sK21_skl,xI) ),
inference(resolution,[status(thm)],[f262,f219]) ).
fof(f306,plain,
( sQ2_spl
| sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f305,f269,f272,f260]) ).
fof(f307,plain,
( ~ sQ7_spl
| ~ iLess0(sbrdtbr0(sK23_skl(sK21_skl)),sbrdtbr0(sK21_skl))
| sK23_skl(sK21_skl) = sz00
| ~ aElementOf0(sK23_skl(sK21_skl),xI) ),
inference(resolution,[status(thm)],[f285,f217]) ).
fof(f310,definition,
( sQ11_spl
<=> iLess0(sbrdtbr0(sK23_skl(sK21_skl)),sbrdtbr0(sK21_skl)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f312,plain,
( sQ11_spl
| ~ iLess0(sbrdtbr0(sK23_skl(sK21_skl)),sbrdtbr0(sK21_skl)) ),
inference(component_clause,[status(thm)],[f310]) ).
fof(f313,plain,
( ~ sQ7_spl
| ~ sQ11_spl
| sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f307,f260,f263,f310,f284]) ).
fof(f322,plain,
( sQ11_spl
| sK21_skl = sz00
| ~ aElementOf0(sK21_skl,xI) ),
inference(resolution,[status(thm)],[f312,f221]) ).
fof(f323,plain,
( sQ11_spl
| sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f322,f269,f272,f310]) ).
fof(f324,plain,
$false,
inference(sat_refutation,[status(thm)],[f275,f277,f279,f287,f292,f306,f313,f323]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG111+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 04:20:17 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 0.13/0.38 % Refutation found
% 0.13/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.46 % Elapsed time: 0.095684 seconds
% 0.13/0.46 % CPU time: 0.108167 seconds
% 0.13/0.46 % Total memory used: 6.693 MB
% 0.13/0.46 % Net memory used: 6.686 MB
%------------------------------------------------------------------------------