%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM393+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 01:40:26 PM UTC 2026
% Result : Theorem 0.08s 0.37s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 7
% Syntax : Number of formulae : 40 ( 7 unt; 2 def)
% Number of atoms : 117 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 127 ( 50 ~; 54 |; 11 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 3 prp; 0-2 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 50 ( 48 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [A,B] :
( ( ordinal(B)
& ordinal(A) )
=> ( ordinal_subset(B,A)
| ordinal_subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B] :
( inclusion_comparable(A,B)
<=> ( subset(B,A)
| subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [A,B] :
( ( ordinal(B)
& ordinal(A) )
=> ( ordinal_subset(A,B)
<=> subset(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A,B] :
( inclusion_comparable(A,B)
=> inclusion_comparable(B,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,conjecture,
! [A] :
( ordinal(A)
=> ! [B] :
( ordinal(B)
=> inclusion_comparable(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
~ ! [A] :
( ordinal(A)
=> ! [B] :
( ordinal(B)
=> inclusion_comparable(A,B) ) ),
inference(negated_conjecture,[status(cth)],[f30]) ).
fof(f54,plain,
! [A,B] :
( ordinal_subset(B,A)
| ordinal_subset(A,B)
| ~ ordinal(B)
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f7]) ).
fof(f55,plain,
! [X0,X1] :
( ordinal_subset(X1,X0)
| ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f56,plain,
! [A,B] :
( ( ( ~ subset(B,A)
& ~ subset(A,B) )
| inclusion_comparable(A,B) )
& ( subset(B,A)
| subset(A,B)
| ~ inclusion_comparable(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f57,plain,
( ! [A,B] :
( ( ~ subset(B,A)
& ~ subset(A,B) )
| inclusion_comparable(A,B) )
& ! [A,B] :
( subset(B,A)
| subset(A,B)
| ~ inclusion_comparable(A,B) ) ),
inference(miniscoping,[status(thm)],[f56]) ).
fof(f59,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| inclusion_comparable(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f60,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| inclusion_comparable(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f105,plain,
! [A,B] :
( ( ordinal_subset(A,B)
<=> subset(A,B) )
| ~ ordinal(B)
| ~ ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f106,plain,
! [A,B] :
( ( ( ~ subset(A,B)
| ordinal_subset(A,B) )
& ( subset(A,B)
| ~ ordinal_subset(A,B) ) )
| ~ ordinal(B)
| ~ ordinal(A) ),
inference(NNF_transformation,[status(thm)],[f105]) ).
fof(f107,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ ordinal_subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f116,plain,
! [A,B] :
( inclusion_comparable(B,A)
| ~ inclusion_comparable(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f117,plain,
! [X0,X1] :
( inclusion_comparable(X1,X0)
| ~ inclusion_comparable(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f120,plain,
? [A] :
( ? [B] :
( ~ inclusion_comparable(A,B)
& ordinal(B) )
& ordinal(A) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f121,plain,
( ~ inclusion_comparable(sK12_skl,sK13_skl)
& ordinal(sK13_skl)
& ordinal(sK12_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(A,sK12_skl),skolemize(B,sK13_skl)],[f120]) ).
fof(f122,plain,
ordinal(sK12_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f123,plain,
ordinal(sK13_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f124,plain,
~ inclusion_comparable(sK12_skl,sK13_skl),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f153,plain,
~ inclusion_comparable(sK13_skl,sK12_skl),
inference(resolution,[status(thm)],[f117,f124]) ).
fof(f163,plain,
! [X0,X1] :
( ordinal_subset(X1,X0)
| ~ ordinal(X0)
| ~ ordinal(X1)
| subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f107,f55]) ).
fof(f164,plain,
! [X0,X1] :
( ordinal_subset(X1,X0)
| subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f163]) ).
fof(f165,plain,
! [X0,X1] :
( subset(X1,X0)
| ~ ordinal(X0)
| ~ ordinal(X1)
| subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f164,f107]) ).
fof(f166,plain,
! [X0,X1] :
( subset(X1,X0)
| subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f165]) ).
fof(f167,plain,
! [X0,X1] :
( inclusion_comparable(X0,X1)
| subset(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(resolution,[status(thm)],[f166,f60]) ).
fof(f169,plain,
! [X0,X1] :
( inclusion_comparable(X0,X1)
| ~ ordinal(X1)
| ~ ordinal(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f167,f59]) ).
fof(f170,plain,
( ~ ordinal(sK12_skl)
| ~ ordinal(sK13_skl) ),
inference(resolution,[status(thm)],[f169,f153]) ).
fof(f172,definition,
( sQ2_spl
<=> ordinal(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f174,plain,
( sQ2_spl
| ~ ordinal(sK13_skl) ),
inference(component_clause,[status(thm)],[f172]) ).
fof(f175,definition,
( sQ3_spl
<=> ordinal(sK12_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f177,plain,
( sQ3_spl
| ~ ordinal(sK12_skl) ),
inference(component_clause,[status(thm)],[f175]) ).
fof(f178,plain,
( ~ sQ3_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f170,f172,f175]) ).
fof(f180,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f174,f123]) ).
fof(f181,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f180]) ).
fof(f182,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f177,f122]) ).
fof(f183,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f182]) ).
fof(f184,plain,
$false,
inference(sat_refutation,[status(thm)],[f178,f181,f183]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM393+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n013.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 02:26:22 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.08/0.37 % Refutation found
% 0.08/0.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.37 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.40 % Elapsed time: 0.033900 seconds
% 0.13/0.40 % CPU time: 0.077193 seconds
% 0.13/0.40 % Total memory used: 15.461 MB
% 0.13/0.40 % Net memory used: 15.453 MB
%------------------------------------------------------------------------------