%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR159+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:14:23 PM UTC 2026
% Result : Theorem 0.46s 1.14s
% Output : CNFRefutation 0.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 5
% Syntax : Number of formulae : 28 ( 10 unt; 0 def)
% Number of atoms : 327 ( 5 equ)
% Maximal formula atoms : 80 ( 11 avg)
% Number of connectives : 431 ( 132 ~; 125 |; 161 &)
% ( 11 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-7 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 234 ( 230 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [CLASS1,CLASS2] :
( p__d__disjoint(CLASS1,CLASS2)
<=> ! [INST] :
( ~ p__d__instance(INST,CLASS2)
| ~ p__d__instance(INST,CLASS1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
( ! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6] :
( p__d__partition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)
<=> ( p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)
& p__d__exhaustiveDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6) ) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5] :
( p__d__partition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)
<=> ( p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)
& p__d__exhaustiveDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5) ) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4] :
( p__d__partition5(CLASS,ROW1,ROW2,ROW3,ROW4)
<=> ( p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)
& p__d__exhaustiveDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4) ) )
& ! [CLASS,ROW1,ROW2,ROW3] :
( p__d__partition4(CLASS,ROW1,ROW2,ROW3)
<=> ( p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3)
& p__d__exhaustiveDecomposition4(CLASS,ROW1,ROW2,ROW3) ) )
& ! [CLASS,ROW1,ROW2] :
( p__d__partition3(CLASS,ROW1,ROW2)
<=> ( p__d__disjointDecomposition3(CLASS,ROW1,ROW2)
& p__d__exhaustiveDecomposition3(CLASS,ROW1,ROW2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
( ! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6] :
( p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)
<=> ( p__d__disjoint(ROW5,ROW6)
& p__d__disjoint(ROW4,ROW6)
& p__d__disjoint(ROW4,ROW5)
& p__d__disjoint(ROW3,ROW6)
& p__d__disjoint(ROW3,ROW5)
& p__d__disjoint(ROW3,ROW4)
& p__d__disjoint(ROW2,ROW6)
& p__d__disjoint(ROW2,ROW5)
& p__d__disjoint(ROW2,ROW4)
& p__d__disjoint(ROW2,ROW3)
& p__d__disjoint(ROW1,ROW6)
& p__d__disjoint(ROW1,ROW5)
& p__d__disjoint(ROW1,ROW4)
& p__d__disjoint(ROW1,ROW3)
& p__d__disjoint(ROW1,ROW2) ) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5] :
( p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)
<=> ( p__d__disjoint(ROW4,ROW5)
& p__d__disjoint(ROW3,ROW5)
& p__d__disjoint(ROW3,ROW4)
& p__d__disjoint(ROW2,ROW5)
& p__d__disjoint(ROW2,ROW4)
& p__d__disjoint(ROW2,ROW3)
& p__d__disjoint(ROW1,ROW5)
& p__d__disjoint(ROW1,ROW4)
& p__d__disjoint(ROW1,ROW3)
& p__d__disjoint(ROW1,ROW2) ) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4] :
( p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)
<=> ( p__d__disjoint(ROW3,ROW4)
& p__d__disjoint(ROW2,ROW4)
& p__d__disjoint(ROW2,ROW3)
& p__d__disjoint(ROW1,ROW4)
& p__d__disjoint(ROW1,ROW3)
& p__d__disjoint(ROW1,ROW2) ) )
& ! [CLASS,ROW1,ROW2,ROW3] :
( p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3)
<=> ( p__d__disjoint(ROW2,ROW3)
& p__d__disjoint(ROW1,ROW3)
& p__d__disjoint(ROW1,ROW2) ) )
& ! [CLASS,ROW1,ROW2] :
( p__d__disjointDecomposition3(CLASS,ROW1,ROW2)
<=> p__d__disjoint(ROW1,ROW2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f290,axiom,
p__d__partition3(c__Integer,c__OddInteger,c__EvenInteger),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7433,conjecture,
! [X,Y] :
( ( p__d__instance(Y,c__OddInteger)
& p__d__instance(X,c__EvenInteger) )
=> X != Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7434,negated_conjecture,
~ ! [X,Y] :
( ( p__d__instance(Y,c__OddInteger)
& p__d__instance(X,c__EvenInteger) )
=> X != Y ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7444,plain,
! [CLASS1,CLASS2] :
( ( ? [INST] :
( p__d__instance(INST,CLASS2)
& p__d__instance(INST,CLASS1) )
| p__d__disjoint(CLASS1,CLASS2) )
& ( ! [INST] :
( ~ p__d__instance(INST,CLASS2)
| ~ p__d__instance(INST,CLASS1) )
| ~ p__d__disjoint(CLASS1,CLASS2) ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f7445,plain,
( ! [CLASS1,CLASS2] :
( ? [INST] :
( p__d__instance(INST,CLASS2)
& p__d__instance(INST,CLASS1) )
| p__d__disjoint(CLASS1,CLASS2) )
& ! [CLASS1,CLASS2] :
( ! [INST] :
( ~ p__d__instance(INST,CLASS2)
| ~ p__d__instance(INST,CLASS1) )
| ~ p__d__disjoint(CLASS1,CLASS2) ) ),
inference(miniscoping,[status(thm)],[f7444]) ).
fof(f7446,plain,
( ! [CLASS1,CLASS2] :
( ( p__d__instance(sK0_skl(CLASS2,CLASS1),CLASS2)
& p__d__instance(sK0_skl(CLASS2,CLASS1),CLASS1) )
| p__d__disjoint(CLASS1,CLASS2) )
& ! [CLASS1,CLASS2] :
( ! [INST] :
( ~ p__d__instance(INST,CLASS2)
| ~ p__d__instance(INST,CLASS1) )
| ~ p__d__disjoint(CLASS1,CLASS2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(INST,sK0_skl(CLASS2,CLASS1))],[f7445]) ).
fof(f7447,plain,
! [X0,X1,X2] :
( ~ p__d__instance(X2,X1)
| ~ p__d__instance(X2,X0)
| ~ p__d__disjoint(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7446]) ).
fof(f7450,plain,
( ! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6] :
( ( ~ p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)
| ~ p__d__exhaustiveDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)
| p__d__partition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6) )
& ( ( p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)
& p__d__exhaustiveDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6) )
| ~ p__d__partition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6) ) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5] :
( ( ~ p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)
| ~ p__d__exhaustiveDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)
| p__d__partition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5) )
& ( ( p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)
& p__d__exhaustiveDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5) )
| ~ p__d__partition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5) ) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4] :
( ( ~ p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)
| ~ p__d__exhaustiveDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)
| p__d__partition5(CLASS,ROW1,ROW2,ROW3,ROW4) )
& ( ( p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)
& p__d__exhaustiveDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4) )
| ~ p__d__partition5(CLASS,ROW1,ROW2,ROW3,ROW4) ) )
& ! [CLASS,ROW1,ROW2,ROW3] :
( ( ~ p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3)
| ~ p__d__exhaustiveDecomposition4(CLASS,ROW1,ROW2,ROW3)
| p__d__partition4(CLASS,ROW1,ROW2,ROW3) )
& ( ( p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3)
& p__d__exhaustiveDecomposition4(CLASS,ROW1,ROW2,ROW3) )
| ~ p__d__partition4(CLASS,ROW1,ROW2,ROW3) ) )
& ! [CLASS,ROW1,ROW2] :
( ( ~ p__d__disjointDecomposition3(CLASS,ROW1,ROW2)
| ~ p__d__exhaustiveDecomposition3(CLASS,ROW1,ROW2)
| p__d__partition3(CLASS,ROW1,ROW2) )
& ( ( p__d__disjointDecomposition3(CLASS,ROW1,ROW2)
& p__d__exhaustiveDecomposition3(CLASS,ROW1,ROW2) )
| ~ p__d__partition3(CLASS,ROW1,ROW2) ) ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f7451,plain,
( ! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6] :
( ~ p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)
| ~ p__d__exhaustiveDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)
| p__d__partition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6] :
( ( p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)
& p__d__exhaustiveDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6) )
| ~ p__d__partition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5] :
( ~ p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)
| ~ p__d__exhaustiveDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)
| p__d__partition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5] :
( ( p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)
& p__d__exhaustiveDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5) )
| ~ p__d__partition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4] :
( ~ p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)
| ~ p__d__exhaustiveDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)
| p__d__partition5(CLASS,ROW1,ROW2,ROW3,ROW4) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4] :
( ( p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)
& p__d__exhaustiveDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4) )
| ~ p__d__partition5(CLASS,ROW1,ROW2,ROW3,ROW4) )
& ! [CLASS,ROW1,ROW2,ROW3] :
( ~ p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3)
| ~ p__d__exhaustiveDecomposition4(CLASS,ROW1,ROW2,ROW3)
| p__d__partition4(CLASS,ROW1,ROW2,ROW3) )
& ! [CLASS,ROW1,ROW2,ROW3] :
( ( p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3)
& p__d__exhaustiveDecomposition4(CLASS,ROW1,ROW2,ROW3) )
| ~ p__d__partition4(CLASS,ROW1,ROW2,ROW3) )
& ! [CLASS,ROW1,ROW2] :
( ~ p__d__disjointDecomposition3(CLASS,ROW1,ROW2)
| ~ p__d__exhaustiveDecomposition3(CLASS,ROW1,ROW2)
| p__d__partition3(CLASS,ROW1,ROW2) )
& ! [CLASS,ROW1,ROW2] :
( ( p__d__disjointDecomposition3(CLASS,ROW1,ROW2)
& p__d__exhaustiveDecomposition3(CLASS,ROW1,ROW2) )
| ~ p__d__partition3(CLASS,ROW1,ROW2) ) ),
inference(miniscoping,[status(thm)],[f7450]) ).
fof(f7453,plain,
! [X0,X1,X2] :
( p__d__disjointDecomposition3(X0,X1,X2)
| ~ p__d__partition3(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f7451]) ).
fof(f7501,plain,
( ! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6] :
( ( ~ p__d__disjoint(ROW5,ROW6)
| ~ p__d__disjoint(ROW4,ROW6)
| ~ p__d__disjoint(ROW4,ROW5)
| ~ p__d__disjoint(ROW3,ROW6)
| ~ p__d__disjoint(ROW3,ROW5)
| ~ p__d__disjoint(ROW3,ROW4)
| ~ p__d__disjoint(ROW2,ROW6)
| ~ p__d__disjoint(ROW2,ROW5)
| ~ p__d__disjoint(ROW2,ROW4)
| ~ p__d__disjoint(ROW2,ROW3)
| ~ p__d__disjoint(ROW1,ROW6)
| ~ p__d__disjoint(ROW1,ROW5)
| ~ p__d__disjoint(ROW1,ROW4)
| ~ p__d__disjoint(ROW1,ROW3)
| ~ p__d__disjoint(ROW1,ROW2)
| p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6) )
& ( ( p__d__disjoint(ROW5,ROW6)
& p__d__disjoint(ROW4,ROW6)
& p__d__disjoint(ROW4,ROW5)
& p__d__disjoint(ROW3,ROW6)
& p__d__disjoint(ROW3,ROW5)
& p__d__disjoint(ROW3,ROW4)
& p__d__disjoint(ROW2,ROW6)
& p__d__disjoint(ROW2,ROW5)
& p__d__disjoint(ROW2,ROW4)
& p__d__disjoint(ROW2,ROW3)
& p__d__disjoint(ROW1,ROW6)
& p__d__disjoint(ROW1,ROW5)
& p__d__disjoint(ROW1,ROW4)
& p__d__disjoint(ROW1,ROW3)
& p__d__disjoint(ROW1,ROW2) )
| ~ p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6) ) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5] :
( ( ~ p__d__disjoint(ROW4,ROW5)
| ~ p__d__disjoint(ROW3,ROW5)
| ~ p__d__disjoint(ROW3,ROW4)
| ~ p__d__disjoint(ROW2,ROW5)
| ~ p__d__disjoint(ROW2,ROW4)
| ~ p__d__disjoint(ROW2,ROW3)
| ~ p__d__disjoint(ROW1,ROW5)
| ~ p__d__disjoint(ROW1,ROW4)
| ~ p__d__disjoint(ROW1,ROW3)
| ~ p__d__disjoint(ROW1,ROW2)
| p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5) )
& ( ( p__d__disjoint(ROW4,ROW5)
& p__d__disjoint(ROW3,ROW5)
& p__d__disjoint(ROW3,ROW4)
& p__d__disjoint(ROW2,ROW5)
& p__d__disjoint(ROW2,ROW4)
& p__d__disjoint(ROW2,ROW3)
& p__d__disjoint(ROW1,ROW5)
& p__d__disjoint(ROW1,ROW4)
& p__d__disjoint(ROW1,ROW3)
& p__d__disjoint(ROW1,ROW2) )
| ~ p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5) ) )
& ! [CLASS,ROW1,ROW2,ROW3,ROW4] :
( ( ~ p__d__disjoint(ROW3,ROW4)
| ~ p__d__disjoint(ROW2,ROW4)
| ~ p__d__disjoint(ROW2,ROW3)
| ~ p__d__disjoint(ROW1,ROW4)
| ~ p__d__disjoint(ROW1,ROW3)
| ~ p__d__disjoint(ROW1,ROW2)
| p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4) )
& ( ( p__d__disjoint(ROW3,ROW4)
& p__d__disjoint(ROW2,ROW4)
& p__d__disjoint(ROW2,ROW3)
& p__d__disjoint(ROW1,ROW4)
& p__d__disjoint(ROW1,ROW3)
& p__d__disjoint(ROW1,ROW2) )
| ~ p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4) ) )
& ! [CLASS,ROW1,ROW2,ROW3] :
( ( ~ p__d__disjoint(ROW2,ROW3)
| ~ p__d__disjoint(ROW1,ROW3)
| ~ p__d__disjoint(ROW1,ROW2)
| p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3) )
& ( ( p__d__disjoint(ROW2,ROW3)
& p__d__disjoint(ROW1,ROW3)
& p__d__disjoint(ROW1,ROW2) )
| ~ p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3) ) )
& ! [CLASS,ROW1,ROW2] :
( ( ~ p__d__disjoint(ROW1,ROW2)
| p__d__disjointDecomposition3(CLASS,ROW1,ROW2) )
& ( p__d__disjoint(ROW1,ROW2)
| ~ p__d__disjointDecomposition3(CLASS,ROW1,ROW2) ) ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f7502,plain,
( ! [ROW1,ROW2,ROW3,ROW4,ROW5,ROW6] :
( ~ p__d__disjoint(ROW5,ROW6)
| ~ p__d__disjoint(ROW4,ROW6)
| ~ p__d__disjoint(ROW4,ROW5)
| ~ p__d__disjoint(ROW3,ROW6)
| ~ p__d__disjoint(ROW3,ROW5)
| ~ p__d__disjoint(ROW3,ROW4)
| ~ p__d__disjoint(ROW2,ROW6)
| ~ p__d__disjoint(ROW2,ROW5)
| ~ p__d__disjoint(ROW2,ROW4)
| ~ p__d__disjoint(ROW2,ROW3)
| ~ p__d__disjoint(ROW1,ROW6)
| ~ p__d__disjoint(ROW1,ROW5)
| ~ p__d__disjoint(ROW1,ROW4)
| ~ p__d__disjoint(ROW1,ROW3)
| ~ p__d__disjoint(ROW1,ROW2)
| ! [CLASS] : p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6) )
& ! [ROW1,ROW2,ROW3,ROW4,ROW5,ROW6] :
( ( p__d__disjoint(ROW5,ROW6)
& p__d__disjoint(ROW4,ROW6)
& p__d__disjoint(ROW4,ROW5)
& p__d__disjoint(ROW3,ROW6)
& p__d__disjoint(ROW3,ROW5)
& p__d__disjoint(ROW3,ROW4)
& p__d__disjoint(ROW2,ROW6)
& p__d__disjoint(ROW2,ROW5)
& p__d__disjoint(ROW2,ROW4)
& p__d__disjoint(ROW2,ROW3)
& p__d__disjoint(ROW1,ROW6)
& p__d__disjoint(ROW1,ROW5)
& p__d__disjoint(ROW1,ROW4)
& p__d__disjoint(ROW1,ROW3)
& p__d__disjoint(ROW1,ROW2) )
| ! [CLASS] : ~ p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6) )
& ! [ROW1,ROW2,ROW3,ROW4,ROW5] :
( ~ p__d__disjoint(ROW4,ROW5)
| ~ p__d__disjoint(ROW3,ROW5)
| ~ p__d__disjoint(ROW3,ROW4)
| ~ p__d__disjoint(ROW2,ROW5)
| ~ p__d__disjoint(ROW2,ROW4)
| ~ p__d__disjoint(ROW2,ROW3)
| ~ p__d__disjoint(ROW1,ROW5)
| ~ p__d__disjoint(ROW1,ROW4)
| ~ p__d__disjoint(ROW1,ROW3)
| ~ p__d__disjoint(ROW1,ROW2)
| ! [CLASS] : p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5) )
& ! [ROW1,ROW2,ROW3,ROW4,ROW5] :
( ( p__d__disjoint(ROW4,ROW5)
& p__d__disjoint(ROW3,ROW5)
& p__d__disjoint(ROW3,ROW4)
& p__d__disjoint(ROW2,ROW5)
& p__d__disjoint(ROW2,ROW4)
& p__d__disjoint(ROW2,ROW3)
& p__d__disjoint(ROW1,ROW5)
& p__d__disjoint(ROW1,ROW4)
& p__d__disjoint(ROW1,ROW3)
& p__d__disjoint(ROW1,ROW2) )
| ! [CLASS] : ~ p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5) )
& ! [ROW1,ROW2,ROW3,ROW4] :
( ~ p__d__disjoint(ROW3,ROW4)
| ~ p__d__disjoint(ROW2,ROW4)
| ~ p__d__disjoint(ROW2,ROW3)
| ~ p__d__disjoint(ROW1,ROW4)
| ~ p__d__disjoint(ROW1,ROW3)
| ~ p__d__disjoint(ROW1,ROW2)
| ! [CLASS] : p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4) )
& ! [ROW1,ROW2,ROW3,ROW4] :
( ( p__d__disjoint(ROW3,ROW4)
& p__d__disjoint(ROW2,ROW4)
& p__d__disjoint(ROW2,ROW3)
& p__d__disjoint(ROW1,ROW4)
& p__d__disjoint(ROW1,ROW3)
& p__d__disjoint(ROW1,ROW2) )
| ! [CLASS] : ~ p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4) )
& ! [ROW1,ROW2,ROW3] :
( ~ p__d__disjoint(ROW2,ROW3)
| ~ p__d__disjoint(ROW1,ROW3)
| ~ p__d__disjoint(ROW1,ROW2)
| ! [CLASS] : p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3) )
& ! [ROW1,ROW2,ROW3] :
( ( p__d__disjoint(ROW2,ROW3)
& p__d__disjoint(ROW1,ROW3)
& p__d__disjoint(ROW1,ROW2) )
| ! [CLASS] : ~ p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3) )
& ! [ROW1,ROW2] :
( ~ p__d__disjoint(ROW1,ROW2)
| ! [CLASS] : p__d__disjointDecomposition3(CLASS,ROW1,ROW2) )
& ! [ROW1,ROW2] :
( p__d__disjoint(ROW1,ROW2)
| ! [CLASS] : ~ p__d__disjointDecomposition3(CLASS,ROW1,ROW2) ) ),
inference(miniscoping,[status(thm)],[f7501]) ).
fof(f7503,plain,
! [X0,X1,X2] :
( p__d__disjoint(X1,X2)
| ~ p__d__disjointDecomposition3(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f7502]) ).
fof(f8028,plain,
p__d__partition3(c__Integer,c__OddInteger,c__EvenInteger),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f23432,plain,
? [X,Y] :
( X = Y
& p__d__instance(Y,c__OddInteger)
& p__d__instance(X,c__EvenInteger) ),
inference(pre_NNF_transformation,[status(thm)],[f7434]) ).
fof(f23433,plain,
( sK1216_skl = sK1217_skl
& p__d__instance(sK1217_skl,c__OddInteger)
& p__d__instance(sK1216_skl,c__EvenInteger) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1216_skl,sK1217_skl]),skolemize(X,sK1216_skl),skolemize(Y,sK1217_skl)],[f23432]) ).
fof(f23434,plain,
p__d__instance(sK1216_skl,c__EvenInteger),
inference(cnf_transformation,[status(thm)],[f23433]) ).
fof(f23435,plain,
p__d__instance(sK1217_skl,c__OddInteger),
inference(cnf_transformation,[status(thm)],[f23433]) ).
fof(f23436,plain,
sK1216_skl = sK1217_skl,
inference(cnf_transformation,[status(thm)],[f23433]) ).
fof(f23755,plain,
p__d__instance(sK1217_skl,c__EvenInteger),
inference(forward_demodulation,[status(thm)],[f23436,f23434]) ).
fof(f23789,plain,
! [X0] :
( ~ p__d__instance(sK1217_skl,X0)
| ~ p__d__disjoint(c__OddInteger,X0) ),
inference(resolution,[status(thm)],[f7447,f23435]) ).
fof(f23810,plain,
~ p__d__disjoint(c__OddInteger,c__EvenInteger),
inference(resolution,[status(thm)],[f23789,f23755]) ).
fof(f23953,plain,
p__d__disjointDecomposition3(c__Integer,c__OddInteger,c__EvenInteger),
inference(resolution,[status(thm)],[f7453,f8028]) ).
fof(f25289,plain,
p__d__disjoint(c__OddInteger,c__EvenInteger),
inference(resolution,[status(thm)],[f7503,f23953]) ).
fof(f25290,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f25289,f23810]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR159+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n003.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 15:15:01 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.32/0.62 % Drodi V4.1.1
% 0.46/1.14 % Refutation found
% 0.46/1.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.46/1.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.46/1.29 % Elapsed time: 0.917475 seconds
% 0.46/1.29 % CPU time: 4.377067 seconds
% 0.46/1.29 % Total memory used: 575.906 MB
% 0.46/1.29 % Net memory used: 572.033 MB
%------------------------------------------------------------------------------