%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR158+1 : TPTP v9.3.1. Released v7.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 12:14:23 PM UTC 2026
% Result : Theorem 0.27s 0.75s
% Output : CNFRefutation 0.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% 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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f212,axiom,
p__d__partition3(c__HumanLanguage,c__NaturalLanguage,c__ConstructedLanguage),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7433,conjecture,
! [X,Y] :
( ( p__d__instance(Y,c__NaturalLanguage)
& p__d__instance(X,c__ConstructedLanguage) )
=> X != Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7434,negated_conjecture,
~ ! [X,Y] :
( ( p__d__instance(Y,c__NaturalLanguage)
& p__d__instance(X,c__ConstructedLanguage) )
=> 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(f7913,plain,
p__d__partition3(c__HumanLanguage,c__NaturalLanguage,c__ConstructedLanguage),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f23432,plain,
? [X,Y] :
( X = Y
& p__d__instance(Y,c__NaturalLanguage)
& p__d__instance(X,c__ConstructedLanguage) ),
inference(pre_NNF_transformation,[status(thm)],[f7434]) ).
fof(f23433,plain,
( sK1216_skl = sK1217_skl
& p__d__instance(sK1217_skl,c__NaturalLanguage)
& p__d__instance(sK1216_skl,c__ConstructedLanguage) ),
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__ConstructedLanguage),
inference(cnf_transformation,[status(thm)],[f23433]) ).
fof(f23435,plain,
p__d__instance(sK1217_skl,c__NaturalLanguage),
inference(cnf_transformation,[status(thm)],[f23433]) ).
fof(f23436,plain,
sK1216_skl = sK1217_skl,
inference(cnf_transformation,[status(thm)],[f23433]) ).
fof(f23773,plain,
p__d__instance(sK1216_skl,c__NaturalLanguage),
inference(forward_demodulation,[status(thm)],[f23436,f23435]) ).
fof(f23813,plain,
p__d__disjointDecomposition3(c__HumanLanguage,c__NaturalLanguage,c__ConstructedLanguage),
inference(resolution,[status(thm)],[f7453,f7913]) ).
fof(f24171,plain,
p__d__disjoint(c__NaturalLanguage,c__ConstructedLanguage),
inference(resolution,[status(thm)],[f7503,f23813]) ).
fof(f24173,plain,
! [X0] :
( ~ p__d__instance(X0,c__ConstructedLanguage)
| ~ p__d__instance(X0,c__NaturalLanguage) ),
inference(resolution,[status(thm)],[f24171,f7447]) ).
fof(f24190,plain,
~ p__d__instance(sK1216_skl,c__ConstructedLanguage),
inference(resolution,[status(thm)],[f24173,f23773]) ).
fof(f24191,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f24190,f23434]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR158+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.52 % Computer : n016.cluster.edu
% 0.11/0.52 % Model : x86_64 x86_64
% 0.11/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.52 % Memory : 8046.5625MB
% 0.11/0.52 % OS : Linux 6.8.0-71-generic
% 0.11/0.52 % CPULimit : 300
% 0.11/0.52 % WCLimit : 300
% 0.11/0.52 % DateTime : Mon Sep 21 15:18:08 UTC 2026
% 0.11/0.53 % CPUTime :
% 0.23/0.64 % Drodi V4.1.1
% 0.27/0.75 % Refutation found
% 0.27/0.75 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.27/0.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.29/0.86 % Elapsed time: 0.321687 seconds
% 0.29/0.86 % CPU time: 1.162828 seconds
% 0.29/0.86 % Total memory used: 564.198 MB
% 0.29/0.86 % Net memory used: 560.130 MB
%------------------------------------------------------------------------------