%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR158+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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 12:15:41 PM UTC 2026
% Result : Theorem 0.48s 0.85s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR158+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n013.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 15:12:51 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.35/0.63 % Drodi V4.1.1
% 0.48/0.85 % Refutation found
% 0.48/0.85 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.48/0.85 % SZS output start CNFRefutation for theBenchmark
% 0.48/0.85 fof(f5,axiom,(
% 0.48/0.85 (! [CLASS1,CLASS2] :( p__d__disjoint(CLASS1,CLASS2)<=> (! [INST] :( ~ p__d__instance(INST,CLASS1)| ~ p__d__instance(INST,CLASS2) ) )) )),
% 0.48/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/0.85 fof(f6,axiom,(
% 0.48/0.85 ( (! [CLASS,ROW1,ROW2] :( p__d__partition3(CLASS,ROW1,ROW2)<=> ( p__d__exhaustiveDecomposition3(CLASS,ROW1,ROW2)& p__d__disjointDecomposition3(CLASS,ROW1,ROW2) ) ))& (! [CLASS,ROW1,ROW2,ROW3] :( p__d__partition4(CLASS,ROW1,ROW2,ROW3)<=> ( p__d__exhaustiveDecomposition4(CLASS,ROW1,ROW2,ROW3)& p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3) ) ))& (! [CLASS,ROW1,ROW2,ROW3,ROW4] :( p__d__partition5(CLASS,ROW1,ROW2,ROW3,ROW4)<=> ( p__d__exhaustiveDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)& p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4) ) ))& (! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5] :( p__d__partition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)<=> ( p__d__exhaustiveDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)& p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5) ) ))& (! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6] :( p__d__partition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)<=> ( p__d__exhaustiveDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)& p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6) ) ) )) ),
% 0.48/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/0.85 fof(f8,axiom,(
% 0.48/0.85 ( (! [CLASS,ROW1,ROW2] :( p__d__disjointDecomposition3(CLASS,ROW1,ROW2)<=> p__d__disjoint(ROW1,ROW2) ))& (! [CLASS,ROW1,ROW2,ROW3] :( p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3)<=> ( p__d__disjoint(ROW1,ROW2)& p__d__disjoint(ROW1,ROW3)& p__d__disjoint(ROW2,ROW3) ) ))& (! [CLASS,ROW1,ROW2,ROW3,ROW4] :( p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)<=> ( p__d__disjoint(ROW1,ROW2)& p__d__disjoint(ROW1,ROW3)& p__d__disjoint(ROW1,ROW4)& p__d__disjoint(ROW2,ROW3)& p__d__disjoint(ROW2,ROW4)& p__d__disjoint(ROW3,ROW4) ) ))& (! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5] :( p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)<=> ( p__d__disjoint(ROW1,ROW2)& p__d__disjoint(ROW1,ROW3)& p__d__disjoint(ROW1,ROW4)& p__d__disjoint(ROW1,ROW5)& p__d__disjoint(ROW2,ROW3)& p__d__disjoint(ROW2,ROW4)& p__d__disjoint(ROW2,ROW5)& p__d__disjoint(ROW3,ROW4)& p__d__disjoint(ROW3,ROW5)& p__d__disjoint(ROW4,ROW5) ) ))& (! [CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6] :( p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)<=> ( p__d__disjoint(ROW1,ROW2)& p__d__disjoint(ROW1,ROW3)& p__d__disjoint(ROW1,ROW4)& p__d__disjoint(ROW1,ROW5)& p__d__disjoint(ROW1,ROW6)& p__d__disjoint(ROW2,ROW3)& p__d__disjoint(ROW2,ROW4)& p__d__disjoint(ROW2,ROW5)& p__d__disjoint(ROW2,ROW6)& p__d__disjoint(ROW3,ROW4)& p__d__disjoint(ROW3,ROW5)& p__d__disjoint(ROW3,ROW6)& p__d__disjoint(ROW4,ROW5)& p__d__disjoint(ROW4,ROW6)& p__d__disjoint(ROW5,ROW6) ) ) )) ),
% 0.48/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/0.85 fof(f212,axiom,(
% 0.48/0.85 p__d__partition3(c__HumanLanguage,c__NaturalLanguage,c__ConstructedLanguage) ),
% 0.48/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/0.85 fof(f7433,conjecture,(
% 0.48/0.85 (! [X,Y] :( ( p__d__instance(X,c__ConstructedLanguage)& p__d__instance(Y,c__NaturalLanguage) )=> X != Y ) )),
% 0.48/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.48/0.85 fof(f7434,negated_conjecture,(
% 0.48/0.85 ~((! [X,Y] :( ( p__d__instance(X,c__ConstructedLanguage)& p__d__instance(Y,c__NaturalLanguage) )=> X != Y ) ))),
% 0.48/0.85 inference(negated_conjecture,[status(cth)],[f7433])).
% 0.48/0.85 fof(f7444,plain,(
% 0.48/0.85 ![CLASS1,CLASS2]: ((~p__d__disjoint(CLASS1,CLASS2)|(![INST]: (~p__d__instance(INST,CLASS1)|~p__d__instance(INST,CLASS2))))&(p__d__disjoint(CLASS1,CLASS2)|(?[INST]: (p__d__instance(INST,CLASS1)&p__d__instance(INST,CLASS2)))))),
% 0.48/0.85 inference(NNF_transformation,[status(thm)],[f5])).
% 0.48/0.85 fof(f7445,plain,(
% 0.48/0.85 (![CLASS1,CLASS2]: (~p__d__disjoint(CLASS1,CLASS2)|(![INST]: (~p__d__instance(INST,CLASS1)|~p__d__instance(INST,CLASS2)))))&(![CLASS1,CLASS2]: (p__d__disjoint(CLASS1,CLASS2)|(?[INST]: (p__d__instance(INST,CLASS1)&p__d__instance(INST,CLASS2)))))),
% 0.48/0.85 inference(miniscoping,[status(thm)],[f7444])).
% 0.48/0.85 fof(f7446,plain,(
% 0.48/0.85 (![CLASS1,CLASS2]: (~p__d__disjoint(CLASS1,CLASS2)|(![INST]: (~p__d__instance(INST,CLASS1)|~p__d__instance(INST,CLASS2)))))&(![CLASS1,CLASS2]: (p__d__disjoint(CLASS1,CLASS2)|(p__d__instance(sK0_skl(CLASS2,CLASS1),CLASS1)&p__d__instance(sK0_skl(CLASS2,CLASS1),CLASS2))))),
% 0.48/0.85 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(INST,sK0_skl(CLASS2,CLASS1))],[f7445])).
% 0.48/0.85 fof(f7447,plain,(
% 0.48/0.85 ![X0,X1,X2]: (~p__d__disjoint(X0,X1)|~p__d__instance(X2,X0)|~p__d__instance(X2,X1))),
% 0.48/0.85 inference(cnf_transformation,[status(thm)],[f7446])).
% 0.48/0.85 fof(f7450,plain,(
% 0.48/0.85 ((((![CLASS,ROW1,ROW2]: ((~p__d__partition3(CLASS,ROW1,ROW2)|(p__d__exhaustiveDecomposition3(CLASS,ROW1,ROW2)&p__d__disjointDecomposition3(CLASS,ROW1,ROW2)))&(p__d__partition3(CLASS,ROW1,ROW2)|(~p__d__exhaustiveDecomposition3(CLASS,ROW1,ROW2)|~p__d__disjointDecomposition3(CLASS,ROW1,ROW2)))))&(![CLASS,ROW1,ROW2,ROW3]: ((~p__d__partition4(CLASS,ROW1,ROW2,ROW3)|(p__d__exhaustiveDecomposition4(CLASS,ROW1,ROW2,ROW3)&p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3)))&(p__d__partition4(CLASS,ROW1,ROW2,ROW3)|(~p__d__exhaustiveDecomposition4(CLASS,ROW1,ROW2,ROW3)|~p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3))))))&(![CLASS,ROW1,ROW2,ROW3,ROW4]: ((~p__d__partition5(CLASS,ROW1,ROW2,ROW3,ROW4)|(p__d__exhaustiveDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)&p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)))&(p__d__partition5(CLASS,ROW1,ROW2,ROW3,ROW4)|(~p__d__exhaustiveDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)|~p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4))))))&(![CLASS,ROW1,ROW2,ROW3,ROW4,ROW5]: ((~p__d__partition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)|(p__d__exhaustiveDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)&p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)))&(p__d__partition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)|(~p__d__exhaustiveDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)|~p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5))))))&(![CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6]: ((~p__d__partition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)|(p__d__exhaustiveDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)&p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)))&(p__d__partition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)|(~p__d__exhaustiveDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)|~p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)))))),
% 0.48/0.85 inference(NNF_transformation,[status(thm)],[f6])).
% 0.48/0.85 fof(f7451,plain,(
% 0.48/0.85 (((((![CLASS,ROW1,ROW2]: (~p__d__partition3(CLASS,ROW1,ROW2)|(p__d__exhaustiveDecomposition3(CLASS,ROW1,ROW2)&p__d__disjointDecomposition3(CLASS,ROW1,ROW2))))&(![CLASS,ROW1,ROW2]: (p__d__partition3(CLASS,ROW1,ROW2)|(~p__d__exhaustiveDecomposition3(CLASS,ROW1,ROW2)|~p__d__disjointDecomposition3(CLASS,ROW1,ROW2)))))&((![CLASS,ROW1,ROW2,ROW3]: (~p__d__partition4(CLASS,ROW1,ROW2,ROW3)|(p__d__exhaustiveDecomposition4(CLASS,ROW1,ROW2,ROW3)&p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3))))&(![CLASS,ROW1,ROW2,ROW3]: (p__d__partition4(CLASS,ROW1,ROW2,ROW3)|(~p__d__exhaustiveDecomposition4(CLASS,ROW1,ROW2,ROW3)|~p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3))))))&((![CLASS,ROW1,ROW2,ROW3,ROW4]: (~p__d__partition5(CLASS,ROW1,ROW2,ROW3,ROW4)|(p__d__exhaustiveDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)&p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4))))&(![CLASS,ROW1,ROW2,ROW3,ROW4]: (p__d__partition5(CLASS,ROW1,ROW2,ROW3,ROW4)|(~p__d__exhaustiveDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)|~p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4))))))&((![CLASS,ROW1,ROW2,ROW3,ROW4,ROW5]: (~p__d__partition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)|(p__d__exhaustiveDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)&p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5))))&(![CLASS,ROW1,ROW2,ROW3,ROW4,ROW5]: (p__d__partition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)|(~p__d__exhaustiveDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)|~p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5))))))&((![CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6]: (~p__d__partition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)|(p__d__exhaustiveDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)&p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6))))&(![CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6]: (p__d__partition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)|(~p__d__exhaustiveDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)|~p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)))))),
% 0.48/0.85 inference(miniscoping,[status(thm)],[f7450])).
% 0.48/0.85 fof(f7453,plain,(
% 0.48/0.85 ![X0,X1,X2]: (~p__d__partition3(X0,X1,X2)|p__d__disjointDecomposition3(X0,X1,X2))),
% 0.48/0.85 inference(cnf_transformation,[status(thm)],[f7451])).
% 0.48/0.85 fof(f7501,plain,(
% 0.48/0.85 ((((![CLASS,ROW1,ROW2]: ((~p__d__disjointDecomposition3(CLASS,ROW1,ROW2)|p__d__disjoint(ROW1,ROW2))&(p__d__disjointDecomposition3(CLASS,ROW1,ROW2)|~p__d__disjoint(ROW1,ROW2))))&(![CLASS,ROW1,ROW2,ROW3]: ((~p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3)|((p__d__disjoint(ROW1,ROW2)&p__d__disjoint(ROW1,ROW3))&p__d__disjoint(ROW2,ROW3)))&(p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3)|((~p__d__disjoint(ROW1,ROW2)|~p__d__disjoint(ROW1,ROW3))|~p__d__disjoint(ROW2,ROW3))))))&(![CLASS,ROW1,ROW2,ROW3,ROW4]: ((~p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)|(((((p__d__disjoint(ROW1,ROW2)&p__d__disjoint(ROW1,ROW3))&p__d__disjoint(ROW1,ROW4))&p__d__disjoint(ROW2,ROW3))&p__d__disjoint(ROW2,ROW4))&p__d__disjoint(ROW3,ROW4)))&(p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4)|(((((~p__d__disjoint(ROW1,ROW2)|~p__d__disjoint(ROW1,ROW3))|~p__d__disjoint(ROW1,ROW4))|~p__d__disjoint(ROW2,ROW3))|~p__d__disjoint(ROW2,ROW4))|~p__d__disjoint(ROW3,ROW4))))))&(![CLASS,ROW1,ROW2,ROW3,ROW4,ROW5]: ((~p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)|(((((((((p__d__disjoint(ROW1,ROW2)&p__d__disjoint(ROW1,ROW3))&p__d__disjoint(ROW1,ROW4))&p__d__disjoint(ROW1,ROW5))&p__d__disjoint(ROW2,ROW3))&p__d__disjoint(ROW2,ROW4))&p__d__disjoint(ROW2,ROW5))&p__d__disjoint(ROW3,ROW4))&p__d__disjoint(ROW3,ROW5))&p__d__disjoint(ROW4,ROW5)))&(p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5)|(((((((((~p__d__disjoint(ROW1,ROW2)|~p__d__disjoint(ROW1,ROW3))|~p__d__disjoint(ROW1,ROW4))|~p__d__disjoint(ROW1,ROW5))|~p__d__disjoint(ROW2,ROW3))|~p__d__disjoint(ROW2,ROW4))|~p__d__disjoint(ROW2,ROW5))|~p__d__disjoint(ROW3,ROW4))|~p__d__disjoint(ROW3,ROW5))|~p__d__disjoint(ROW4,ROW5))))))&(![CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6]: ((~p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)|((((((((((((((p__d__disjoint(ROW1,ROW2)&p__d__disjoint(ROW1,ROW3))&p__d__disjoint(ROW1,ROW4))&p__d__disjoint(ROW1,ROW5))&p__d__disjoint(ROW1,ROW6))&p__d__disjoint(ROW2,ROW3))&p__d__disjoint(ROW2,ROW4))&p__d__disjoint(ROW2,ROW5))&p__d__disjoint(ROW2,ROW6))&p__d__disjoint(ROW3,ROW4))&p__d__disjoint(ROW3,ROW5))&p__d__disjoint(ROW3,ROW6))&p__d__disjoint(ROW4,ROW5))&p__d__disjoint(ROW4,ROW6))&p__d__disjoint(ROW5,ROW6)))&(p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6)|((((((((((((((~p__d__disjoint(ROW1,ROW2)|~p__d__disjoint(ROW1,ROW3))|~p__d__disjoint(ROW1,ROW4))|~p__d__disjoint(ROW1,ROW5))|~p__d__disjoint(ROW1,ROW6))|~p__d__disjoint(ROW2,ROW3))|~p__d__disjoint(ROW2,ROW4))|~p__d__disjoint(ROW2,ROW5))|~p__d__disjoint(ROW2,ROW6))|~p__d__disjoint(ROW3,ROW4))|~p__d__disjoint(ROW3,ROW5))|~p__d__disjoint(ROW3,ROW6))|~p__d__disjoint(ROW4,ROW5))|~p__d__disjoint(ROW4,ROW6))|~p__d__disjoint(ROW5,ROW6)))))),
% 0.48/0.85 inference(NNF_transformation,[status(thm)],[f8])).
% 0.48/0.85 fof(f7502,plain,(
% 0.48/0.85 (((((![ROW1,ROW2]: ((![CLASS]: ~p__d__disjointDecomposition3(CLASS,ROW1,ROW2))|p__d__disjoint(ROW1,ROW2)))&(![ROW1,ROW2]: ((![CLASS]: p__d__disjointDecomposition3(CLASS,ROW1,ROW2))|~p__d__disjoint(ROW1,ROW2))))&((![ROW1,ROW2,ROW3]: ((![CLASS]: ~p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3))|((p__d__disjoint(ROW1,ROW2)&p__d__disjoint(ROW1,ROW3))&p__d__disjoint(ROW2,ROW3))))&(![ROW1,ROW2,ROW3]: ((![CLASS]: p__d__disjointDecomposition4(CLASS,ROW1,ROW2,ROW3))|((~p__d__disjoint(ROW1,ROW2)|~p__d__disjoint(ROW1,ROW3))|~p__d__disjoint(ROW2,ROW3))))))&((![ROW1,ROW2,ROW3,ROW4]: ((![CLASS]: ~p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4))|(((((p__d__disjoint(ROW1,ROW2)&p__d__disjoint(ROW1,ROW3))&p__d__disjoint(ROW1,ROW4))&p__d__disjoint(ROW2,ROW3))&p__d__disjoint(ROW2,ROW4))&p__d__disjoint(ROW3,ROW4))))&(![ROW1,ROW2,ROW3,ROW4]: ((![CLASS]: p__d__disjointDecomposition5(CLASS,ROW1,ROW2,ROW3,ROW4))|(((((~p__d__disjoint(ROW1,ROW2)|~p__d__disjoint(ROW1,ROW3))|~p__d__disjoint(ROW1,ROW4))|~p__d__disjoint(ROW2,ROW3))|~p__d__disjoint(ROW2,ROW4))|~p__d__disjoint(ROW3,ROW4))))))&((![ROW1,ROW2,ROW3,ROW4,ROW5]: ((![CLASS]: ~p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5))|(((((((((p__d__disjoint(ROW1,ROW2)&p__d__disjoint(ROW1,ROW3))&p__d__disjoint(ROW1,ROW4))&p__d__disjoint(ROW1,ROW5))&p__d__disjoint(ROW2,ROW3))&p__d__disjoint(ROW2,ROW4))&p__d__disjoint(ROW2,ROW5))&p__d__disjoint(ROW3,ROW4))&p__d__disjoint(ROW3,ROW5))&p__d__disjoint(ROW4,ROW5))))&(![ROW1,ROW2,ROW3,ROW4,ROW5]: ((![CLASS]: p__d__disjointDecomposition6(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5))|(((((((((~p__d__disjoint(ROW1,ROW2)|~p__d__disjoint(ROW1,ROW3))|~p__d__disjoint(ROW1,ROW4))|~p__d__disjoint(ROW1,ROW5))|~p__d__disjoint(ROW2,ROW3))|~p__d__disjoint(ROW2,ROW4))|~p__d__disjoint(ROW2,ROW5))|~p__d__disjoint(ROW3,ROW4))|~p__d__disjoint(ROW3,ROW5))|~p__d__disjoint(ROW4,ROW5))))))&((![ROW1,ROW2,ROW3,ROW4,ROW5,ROW6]: ((![CLASS]: ~p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6))|((((((((((((((p__d__disjoint(ROW1,ROW2)&p__d__disjoint(ROW1,ROW3))&p__d__disjoint(ROW1,ROW4))&p__d__disjoint(ROW1,ROW5))&p__d__disjoint(ROW1,ROW6))&p__d__disjoint(ROW2,ROW3))&p__d__disjoint(ROW2,ROW4))&p__d__disjoint(ROW2,ROW5))&p__d__disjoint(ROW2,ROW6))&p__d__disjoint(ROW3,ROW4))&p__d__disjoint(ROW3,ROW5))&p__d__disjoint(ROW3,ROW6))&p__d__disjoint(ROW4,ROW5))&p__d__disjoint(ROW4,ROW6))&p__d__disjoint(ROW5,ROW6))))&(![ROW1,ROW2,ROW3,ROW4,ROW5,ROW6]: ((![CLASS]: p__d__disjointDecomposition7(CLASS,ROW1,ROW2,ROW3,ROW4,ROW5,ROW6))|((((((((((((((~p__d__disjoint(ROW1,ROW2)|~p__d__disjoint(ROW1,ROW3))|~p__d__disjoint(ROW1,ROW4))|~p__d__disjoint(ROW1,ROW5))|~p__d__disjoint(ROW1,ROW6))|~p__d__disjoint(ROW2,ROW3))|~p__d__disjoint(ROW2,ROW4))|~p__d__disjoint(ROW2,ROW5))|~p__d__disjoint(ROW2,ROW6))|~p__d__disjoint(ROW3,ROW4))|~p__d__disjoint(ROW3,ROW5))|~p__d__disjoint(ROW3,ROW6))|~p__d__disjoint(ROW4,ROW5))|~p__d__disjoint(ROW4,ROW6))|~p__d__disjoint(ROW5,ROW6)))))),
% 0.48/0.85 inference(miniscoping,[status(thm)],[f7501])).
% 0.48/0.85 fof(f7503,plain,(
% 0.48/0.85 ![X0,X1,X2]: (~p__d__disjointDecomposition3(X0,X1,X2)|p__d__disjoint(X1,X2))),
% 0.48/0.85 inference(cnf_transformation,[status(thm)],[f7502])).
% 0.48/0.85 fof(f7913,plain,(
% 0.48/0.85 p__d__partition3(c__HumanLanguage,c__NaturalLanguage,c__ConstructedLanguage)),
% 0.48/0.85 inference(cnf_transformation,[status(thm)],[f212])).
% 0.48/0.85 fof(f23432,plain,(
% 0.48/0.85 (?[X,Y]: ((p__d__instance(X,c__ConstructedLanguage)&p__d__instance(Y,c__NaturalLanguage))&X=Y))),
% 0.48/0.85 inference(pre_NNF_transformation,[status(thm)],[f7434])).
% 0.48/0.85 fof(f23433,plain,(
% 0.48/0.85 ((p__d__instance(sK1216_skl,c__ConstructedLanguage)&p__d__instance(sK1217_skl,c__NaturalLanguage))&sK1216_skl=sK1217_skl)),
% 0.48/0.85 inference(skolemize,[status(esa),new_symbols(skolem,[sK1216_skl,sK1217_skl]),skolemize(X,sK1216_skl),skolemize(Y,sK1217_skl)],[f23432])).
% 0.48/0.85 fof(f23434,plain,(
% 0.48/0.85 p__d__instance(sK1216_skl,c__ConstructedLanguage)),
% 0.48/0.85 inference(cnf_transformation,[status(thm)],[f23433])).
% 0.48/0.85 fof(f23435,plain,(
% 0.48/0.85 p__d__instance(sK1217_skl,c__NaturalLanguage)),
% 0.48/0.85 inference(cnf_transformation,[status(thm)],[f23433])).
% 0.48/0.85 fof(f23436,plain,(
% 0.48/0.85 sK1216_skl=sK1217_skl),
% 0.48/0.85 inference(cnf_transformation,[status(thm)],[f23433])).
% 0.48/0.85 fof(f23773,plain,(
% 0.48/0.85 p__d__instance(sK1216_skl,c__NaturalLanguage)),
% 0.48/0.85 inference(forward_demodulation,[status(thm)],[f23436,f23435])).
% 0.48/0.85 fof(f23813,plain,(
% 0.48/0.85 p__d__disjointDecomposition3(c__HumanLanguage,c__NaturalLanguage,c__ConstructedLanguage)),
% 0.48/0.85 inference(resolution,[status(thm)],[f7453,f7913])).
% 0.48/0.85 fof(f24171,plain,(
% 0.48/0.85 p__d__disjoint(c__NaturalLanguage,c__ConstructedLanguage)),
% 0.48/0.85 inference(resolution,[status(thm)],[f7503,f23813])).
% 0.48/0.85 fof(f24173,plain,(
% 0.48/0.85 ![X0]: (~p__d__instance(X0,c__NaturalLanguage)|~p__d__instance(X0,c__ConstructedLanguage))),
% 0.48/0.85 inference(resolution,[status(thm)],[f24171,f7447])).
% 0.48/0.85 fof(f24190,plain,(
% 0.49/0.90 ~p__d__instance(sK1216_skl,c__NaturalLanguage)),
% 0.49/0.90 inference(resolution,[status(thm)],[f24173,f23434])).
% 0.49/0.90 fof(f24191,plain,(
% 0.49/0.90 $false),
% 0.49/0.90 inference(forward_subsumption_resolution,[status(thm)],[f24190,f23773])).
% 0.49/0.90 % SZS output end CNFRefutation for theBenchmark.p
% 0.49/0.94 % Elapsed time: 0.556689 seconds
% 0.49/0.94 % CPU time: 2.039924 seconds
% 0.49/0.94 % Total memory used: 566.591 MB
% 0.49/0.94 % Net memory used: 562.838 MB
%------------------------------------------------------------------------------