%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR159+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 : 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:15:41 PM UTC 2026
% Result : Theorem 3.74s 1.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR159+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.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 15:15:02 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.40/0.67 % Drodi V4.1.1
% 3.74/1.21 % Refutation found
% 3.74/1.21 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.74/1.21 % SZS output start CNFRefutation for theBenchmark
% 3.74/1.21 fof(f5,axiom,(
% 3.74/1.21 (! [CLASS1,CLASS2] :( p__d__disjoint(CLASS1,CLASS2)<=> (! [INST] :( ~ p__d__instance(INST,CLASS1)| ~ p__d__instance(INST,CLASS2) ) )) )),
% 3.74/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.74/1.21 fof(f6,axiom,(
% 3.74/1.21 ( (! [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) ) ) )) ),
% 3.74/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.74/1.21 fof(f8,axiom,(
% 3.74/1.21 ( (! [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) ) ) )) ),
% 3.74/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.74/1.21 fof(f290,axiom,(
% 3.74/1.21 p__d__partition3(c__Integer,c__OddInteger,c__EvenInteger) ),
% 3.74/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.74/1.21 fof(f7433,conjecture,(
% 3.74/1.21 (! [X,Y] :( ( p__d__instance(X,c__EvenInteger)& p__d__instance(Y,c__OddInteger) )=> X != Y ) )),
% 3.74/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.74/1.21 fof(f7434,negated_conjecture,(
% 3.74/1.21 ~((! [X,Y] :( ( p__d__instance(X,c__EvenInteger)& p__d__instance(Y,c__OddInteger) )=> X != Y ) ))),
% 3.74/1.21 inference(negated_conjecture,[status(cth)],[f7433])).
% 3.74/1.21 fof(f7444,plain,(
% 3.74/1.21 ![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)))))),
% 3.74/1.21 inference(NNF_transformation,[status(thm)],[f5])).
% 3.74/1.21 fof(f7445,plain,(
% 3.74/1.21 (![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)))))),
% 3.74/1.21 inference(miniscoping,[status(thm)],[f7444])).
% 3.74/1.21 fof(f7446,plain,(
% 3.74/1.21 (![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))))),
% 3.74/1.21 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(INST,sK0_skl(CLASS2,CLASS1))],[f7445])).
% 3.74/1.21 fof(f7447,plain,(
% 3.74/1.21 ![X0,X1,X2]: (~p__d__disjoint(X0,X1)|~p__d__instance(X2,X0)|~p__d__instance(X2,X1))),
% 3.74/1.21 inference(cnf_transformation,[status(thm)],[f7446])).
% 3.74/1.21 fof(f7450,plain,(
% 3.74/1.21 ((((![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)))))),
% 3.74/1.21 inference(NNF_transformation,[status(thm)],[f6])).
% 3.74/1.21 fof(f7451,plain,(
% 3.74/1.21 (((((![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)))))),
% 3.74/1.21 inference(miniscoping,[status(thm)],[f7450])).
% 3.74/1.21 fof(f7453,plain,(
% 3.74/1.21 ![X0,X1,X2]: (~p__d__partition3(X0,X1,X2)|p__d__disjointDecomposition3(X0,X1,X2))),
% 3.74/1.21 inference(cnf_transformation,[status(thm)],[f7451])).
% 3.74/1.21 fof(f7501,plain,(
% 3.74/1.21 ((((![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)))))),
% 3.74/1.21 inference(NNF_transformation,[status(thm)],[f8])).
% 3.74/1.21 fof(f7502,plain,(
% 3.74/1.21 (((((![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)))))),
% 3.74/1.21 inference(miniscoping,[status(thm)],[f7501])).
% 3.74/1.21 fof(f7503,plain,(
% 3.74/1.21 ![X0,X1,X2]: (~p__d__disjointDecomposition3(X0,X1,X2)|p__d__disjoint(X1,X2))),
% 3.74/1.21 inference(cnf_transformation,[status(thm)],[f7502])).
% 3.74/1.21 fof(f8028,plain,(
% 3.74/1.21 p__d__partition3(c__Integer,c__OddInteger,c__EvenInteger)),
% 3.74/1.21 inference(cnf_transformation,[status(thm)],[f290])).
% 3.74/1.21 fof(f23432,plain,(
% 3.74/1.21 (?[X,Y]: ((p__d__instance(X,c__EvenInteger)&p__d__instance(Y,c__OddInteger))&X=Y))),
% 3.74/1.21 inference(pre_NNF_transformation,[status(thm)],[f7434])).
% 3.74/1.21 fof(f23433,plain,(
% 3.74/1.21 ((p__d__instance(sK1216_skl,c__EvenInteger)&p__d__instance(sK1217_skl,c__OddInteger))&sK1216_skl=sK1217_skl)),
% 3.74/1.21 inference(skolemize,[status(esa),new_symbols(skolem,[sK1216_skl,sK1217_skl]),skolemize(X,sK1216_skl),skolemize(Y,sK1217_skl)],[f23432])).
% 3.74/1.21 fof(f23434,plain,(
% 3.74/1.21 p__d__instance(sK1216_skl,c__EvenInteger)),
% 3.74/1.21 inference(cnf_transformation,[status(thm)],[f23433])).
% 3.74/1.21 fof(f23435,plain,(
% 3.74/1.21 p__d__instance(sK1217_skl,c__OddInteger)),
% 3.74/1.21 inference(cnf_transformation,[status(thm)],[f23433])).
% 3.74/1.21 fof(f23436,plain,(
% 3.74/1.21 sK1216_skl=sK1217_skl),
% 3.74/1.21 inference(cnf_transformation,[status(thm)],[f23433])).
% 3.74/1.21 fof(f23608,plain,(
% 3.74/1.21 p__d__instance(sK1216_skl,c__OddInteger)),
% 3.74/1.21 inference(forward_demodulation,[status(thm)],[f23436,f23435])).
% 3.74/1.21 fof(f23634,plain,(
% 3.74/1.21 ![X0]: (~p__d__disjoint(c__OddInteger,X0)|~p__d__instance(sK1216_skl,X0))),
% 3.74/1.21 inference(resolution,[status(thm)],[f7447,f23608])).
% 3.74/1.21 fof(f23672,plain,(
% 3.74/1.21 p__d__disjointDecomposition3(c__Integer,c__OddInteger,c__EvenInteger)),
% 3.74/1.21 inference(resolution,[status(thm)],[f7453,f8028])).
% 3.74/1.21 fof(f24195,plain,(
% 3.74/1.21 p__d__disjoint(c__OddInteger,c__EvenInteger)),
% 3.74/1.21 inference(resolution,[status(thm)],[f7503,f23672])).
% 3.74/1.21 fof(f24208,plain,(
% 3.74/1.21 ~p__d__instance(sK1216_skl,c__EvenInteger)),
% 3.74/1.21 inference(resolution,[status(thm)],[f24195,f23634])).
% 3.74/1.21 fof(f24212,plain,(
% 3.74/1.21 $false),
% 3.74/1.21 inference(forward_subsumption_resolution,[status(thm)],[f24208,f23434])).
% 3.74/1.28 % SZS output end CNFRefutation for theBenchmark.p
% 0.52/1.31 % Elapsed time: 0.930271 seconds
% 0.52/1.31 % CPU time: 4.476465 seconds
% 0.52/1.31 % Total memory used: 572.273 MB
% 0.52/1.31 % Net memory used: 568.112 MB
%------------------------------------------------------------------------------