%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET988+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:11:06 PM UTC 2026
% Result : Theorem 0.13s 5.40s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 3
% Syntax : Number of formulae : 32 ( 4 unt; 0 def)
% Number of atoms : 123 ( 33 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 148 ( 57 ~; 51 |; 31 &)
% ( 4 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 1 con; 0-2 aty)
% Number of variables : 102 ( 82 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f31,conjecture,
! [A] :
( ( ! [B,C,D] :
( ( in(ordered_pair(B,D),A)
& in(ordered_pair(B,C),A) )
=> C = D )
& ! [B] :
~ ( ! [C,D] : ordered_pair(C,D) != B
& in(B,A) ) )
=> ( function(A)
& relation(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
~ ! [A] :
( ( ! [B,C,D] :
( ( in(ordered_pair(B,D),A)
& in(ordered_pair(B,C),A) )
=> C = D )
& ! [B] :
~ ( ! [C,D] : ordered_pair(C,D) != B
& in(B,A) ) )
=> ( function(A)
& relation(A) ) ),
inference(negated_conjecture,[status(cth)],[f31]) ).
fof(f33,axiom,
! [A] :
( function(A)
<=> ! [B,C,D] :
( ( in(ordered_pair(B,D),A)
& in(ordered_pair(B,C),A) )
=> C = D ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [A] :
( relation(A)
<=> ! [B] :
~ ( ! [C,D] : B != ordered_pair(C,D)
& in(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,plain,
? [A] :
( ( ~ function(A)
| ~ relation(A) )
& ! [B,C,D] :
( C = D
| ~ in(ordered_pair(B,D),A)
| ~ in(ordered_pair(B,C),A) )
& ! [B] :
( ? [C,D] : ordered_pair(C,D) = B
| ~ in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f103,plain,
? [A] :
( ( ~ function(A)
| ~ relation(A) )
& ! [C,D] :
( C = D
| ! [B] :
( ~ in(ordered_pair(B,D),A)
| ~ in(ordered_pair(B,C),A) ) )
& ! [B] :
( ? [C,D] : ordered_pair(C,D) = B
| ~ in(B,A) ) ),
inference(miniscoping,[status(thm)],[f102]) ).
fof(f104,plain,
( ( ~ function(sK9_skl)
| ~ relation(sK9_skl) )
& ! [C,D] :
( C = D
| ! [B] :
( ~ in(ordered_pair(B,D),sK9_skl)
| ~ in(ordered_pair(B,C),sK9_skl) ) )
& ! [B] :
( ordered_pair(sK10_skl(B),sK11_skl(B)) = B
| ~ in(B,sK9_skl) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl]),skolemize(A,sK9_skl),skolemize(C,sK10_skl(B)),skolemize(D,sK11_skl(B))],[f103]) ).
fof(f105,plain,
! [X0] :
( ordered_pair(sK10_skl(X0),sK11_skl(X0)) = X0
| ~ in(X0,sK9_skl) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f106,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ in(ordered_pair(X0,X2),sK9_skl)
| ~ in(ordered_pair(X0,X1),sK9_skl) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f107,plain,
( ~ function(sK9_skl)
| ~ relation(sK9_skl) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f108,plain,
! [A] :
( function(A)
<=> ! [B,C,D] :
( C = D
| ~ in(ordered_pair(B,D),A)
| ~ in(ordered_pair(B,C),A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f109,plain,
! [A] :
( ( ? [B,C,D] :
( C != D
& in(ordered_pair(B,D),A)
& in(ordered_pair(B,C),A) )
| function(A) )
& ( ! [B,C,D] :
( C = D
| ~ in(ordered_pair(B,D),A)
| ~ in(ordered_pair(B,C),A) )
| ~ function(A) ) ),
inference(NNF_transformation,[status(thm)],[f108]) ).
fof(f110,plain,
( ! [A] :
( ? [C,D] :
( C != D
& ? [B] :
( in(ordered_pair(B,D),A)
& in(ordered_pair(B,C),A) ) )
| function(A) )
& ! [A] :
( ! [C,D] :
( C = D
| ! [B] :
( ~ in(ordered_pair(B,D),A)
| ~ in(ordered_pair(B,C),A) ) )
| ~ function(A) ) ),
inference(miniscoping,[status(thm)],[f109]) ).
fof(f111,plain,
( ! [A] :
( ( sK12_skl(A) != sK13_skl(A)
& in(ordered_pair(sK14_skl(A),sK13_skl(A)),A)
& in(ordered_pair(sK14_skl(A),sK12_skl(A)),A) )
| function(A) )
& ! [A] :
( ! [C,D] :
( C = D
| ! [B] :
( ~ in(ordered_pair(B,D),A)
| ~ in(ordered_pair(B,C),A) ) )
| ~ function(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(C,sK12_skl(A)),skolemize(D,sK13_skl(A)),skolemize(B,sK14_skl(A))],[f110]) ).
fof(f113,plain,
! [X0] :
( in(ordered_pair(sK14_skl(X0),sK12_skl(X0)),X0)
| function(X0) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f114,plain,
! [X0] :
( in(ordered_pair(sK14_skl(X0),sK13_skl(X0)),X0)
| function(X0) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f115,plain,
! [X0] :
( sK12_skl(X0) != sK13_skl(X0)
| function(X0) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f116,plain,
! [A] :
( relation(A)
<=> ! [B] :
( ? [C,D] : B = ordered_pair(C,D)
| ~ in(B,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f117,plain,
! [A] :
( ( ? [B] :
( ! [C,D] : B != ordered_pair(C,D)
& in(B,A) )
| relation(A) )
& ( ! [B] :
( ? [C,D] : B = ordered_pair(C,D)
| ~ in(B,A) )
| ~ relation(A) ) ),
inference(NNF_transformation,[status(thm)],[f116]) ).
fof(f118,plain,
( ! [A] :
( ? [B] :
( ! [C,D] : B != ordered_pair(C,D)
& in(B,A) )
| relation(A) )
& ! [A] :
( ! [B] :
( ? [C,D] : B = ordered_pair(C,D)
| ~ in(B,A) )
| ~ relation(A) ) ),
inference(miniscoping,[status(thm)],[f117]) ).
fof(f119,plain,
( ! [A] :
( ( ! [C,D] : sK17_skl(A) != ordered_pair(C,D)
& in(sK17_skl(A),A) )
| relation(A) )
& ! [A] :
( ! [B] :
( B = ordered_pair(sK15_skl(B,A),sK16_skl(B,A))
| ~ in(B,A) )
| ~ relation(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(C,sK15_skl(B,A)),skolemize(D,sK16_skl(B,A)),skolemize(B,sK17_skl(A))],[f118]) ).
fof(f121,plain,
! [X0] :
( in(sK17_skl(X0),X0)
| relation(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f122,plain,
! [X0,X1,X2] :
( sK17_skl(X0) != ordered_pair(X1,X2)
| relation(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f185,plain,
! [X0] :
( X0 = sK12_skl(sK9_skl)
| ~ in(ordered_pair(sK14_skl(sK9_skl),X0),sK9_skl)
| function(sK9_skl) ),
inference(resolution,[status(thm)],[f113,f106]) ).
fof(f193,plain,
! [X0] :
( ~ in(sK17_skl(X0),sK9_skl)
| relation(X0) ),
inference(resolution,[status(thm)],[f122,f105]) ).
fof(f202,plain,
( relation(sK9_skl)
| relation(sK9_skl) ),
inference(resolution,[status(thm)],[f193,f121]) ).
fof(f203,plain,
relation(sK9_skl),
inference(duplicate_literals_removal,[status(thm)],[f202]) ).
fof(f204,plain,
~ function(sK9_skl),
inference(backward_subsumption_resolution,[status(thm)],[f107,f203]) ).
fof(f214,plain,
! [X0] :
( X0 = sK12_skl(sK9_skl)
| ~ in(ordered_pair(sK14_skl(sK9_skl),X0),sK9_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f185,f204]) ).
fof(f215,plain,
( function(sK9_skl)
| sK13_skl(sK9_skl) = sK12_skl(sK9_skl) ),
inference(resolution,[status(thm)],[f214,f114]) ).
fof(f217,plain,
function(sK9_skl),
inference(forward_subsumption_resolution,[status(thm)],[f215,f115]) ).
fof(f218,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f217,f204]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET988+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n015.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 05:49:57 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.38 % Drodi V4.1.1
% 0.13/5.40 % Refutation found
% 0.13/5.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/5.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/5.43 % Elapsed time: 0.049599 seconds
% 0.13/5.43 % CPU time: 0.142995 seconds
% 0.13/5.43 % Total memory used: 74.222 MB
% 0.13/5.43 % Net memory used: 74.144 MB
%------------------------------------------------------------------------------