%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU425+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:22:37 PM UTC 2026
% Result : Theorem 2.23s 0.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU425+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n001.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Mon Sep 21 06:32:29 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.46 % Drodi V4.1.1
% 2.23/0.80 % Refutation found
% 2.23/0.80 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.23/0.80 % SZS output start CNFRefutation for theBenchmark
% 2.23/0.80 fof(f1,conjecture,(
% 2.23/0.80 (! [A,B,C] :( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))=> ( v1_funct_1(k5_relset_2(A,C))& v1_funct_2(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))& m2_relset_1(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C))) ) ) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f2,negated_conjecture,(
% 2.23/0.80 ~((! [A,B,C] :( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))=> ( v1_funct_1(k5_relset_2(A,C))& v1_funct_2(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))& m2_relset_1(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C))) ) ) ))),
% 2.23/0.80 inference(negated_conjecture,[status(cth)],[f1])).
% 2.23/0.80 fof(f5,axiom,(
% 2.23/0.80 (! [A,B,C] :( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))=> v1_relat_1(C) ) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f6,axiom,(
% 2.23/0.80 (! [A,B,C] :( m2_relset_1(C,A,B)=> ( ( ( B = k1_xboole_0=> A = k1_xboole_0 )=> ( v1_funct_2(C,A,B)<=> A = k4_relset_1(A,B,C) ) )& ( B = k1_xboole_0=> ( A = k1_xboole_0| ( v1_funct_2(C,A,B)<=> C = k1_xboole_0 ) ) ) ) ) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f7,axiom,(
% 2.23/0.80 (! [A,B] :( v1_relat_1(B)=> (! [C] :( ( v1_relat_1(C)& v1_funct_1(C) )=> ( C = k5_relset_2(A,B)<=> ( k1_relat_1(C) = k1_zfmisc_1(A)& (! [D] :( r1_tarski(D,A)=> k1_funct_1(C,D) = k9_relat_1(B,D) ) )) ) ) )) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f15,axiom,(
% 2.23/0.80 (! [A,B] :( v1_relat_1(B)=> ( v1_relat_1(k5_relset_2(A,B))& v1_funct_1(k5_relset_2(A,B)) ) ) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f19,axiom,(
% 2.23/0.80 (! [A,B,C] :( m2_relset_1(C,A,B)=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f24,axiom,(
% 2.23/0.80 (! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f32,axiom,(
% 2.23/0.80 (? [A] :( v1_xboole_0(A)& v1_relat_1(A) ) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f38,axiom,(
% 2.23/0.80 (! [A,B,C] :( m1_relset_1(C,A,B)=> k4_relset_1(A,B,C) = k1_relat_1(C) ) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f39,axiom,(
% 2.23/0.80 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f40,axiom,(
% 2.23/0.80 (! [A,B] : r1_tarski(A,A) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f41,axiom,(
% 2.23/0.80 (! [A,B,C] :( v1_relat_1(C)=> ( ( r1_tarski(k1_relat_1(C),A)& r1_tarski(k2_relat_1(C),B) )=> m2_relset_1(C,A,B) ) ) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f43,axiom,(
% 2.23/0.80 (! [A,B,C] :( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))=> r1_tarski(k2_relat_1(k5_relset_2(A,C)),k1_zfmisc_1(k2_relat_1(C))) ) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f48,axiom,(
% 2.23/0.80 (! [A] :( v1_xboole_0(A)=> A = k1_xboole_0 ) )),
% 2.23/0.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.23/0.80 fof(f51,plain,(
% 2.23/0.80 (?[A,B,C]: (m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))&((~v1_funct_1(k5_relset_2(A,C))|~v1_funct_2(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C))))|~m2_relset_1(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C))))))),
% 2.23/0.80 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 2.23/0.80 fof(f52,plain,(
% 2.23/0.80 ?[A,C]: ((?[B]: m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))))&((~v1_funct_1(k5_relset_2(A,C))|~v1_funct_2(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C))))|~m2_relset_1(k5_relset_2(A,C),k1_zfmisc_1(A),k1_zfmisc_1(k2_relat_1(C)))))),
% 2.23/0.80 inference(miniscoping,[status(thm)],[f51])).
% 2.23/0.80 fof(f53,plain,(
% 2.23/0.80 (m1_subset_1(sK1_skl,k1_zfmisc_1(k2_zfmisc_1(sK0_skl,sK2_skl)))&((~v1_funct_1(k5_relset_2(sK0_skl,sK1_skl))|~v1_funct_2(k5_relset_2(sK0_skl,sK1_skl),k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl))))|~m2_relset_1(k5_relset_2(sK0_skl,sK1_skl),k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)))))),
% 2.23/0.80 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(A,sK0_skl),skolemize(C,sK1_skl),skolemize(B,sK2_skl)],[f52])).
% 2.23/0.80 fof(f54,plain,(
% 2.23/0.80 m1_subset_1(sK1_skl,k1_zfmisc_1(k2_zfmisc_1(sK0_skl,sK2_skl)))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f53])).
% 2.23/0.80 fof(f55,plain,(
% 2.23/0.80 ~v1_funct_1(k5_relset_2(sK0_skl,sK1_skl))|~v1_funct_2(k5_relset_2(sK0_skl,sK1_skl),k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)))|~m2_relset_1(k5_relset_2(sK0_skl,sK1_skl),k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f53])).
% 2.23/0.80 fof(f60,plain,(
% 2.23/0.80 ![A,B,C]: (~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))|v1_relat_1(C))),
% 2.23/0.80 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 2.23/0.80 fof(f61,plain,(
% 2.23/0.80 ![C]: ((![A,B]: ~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))))|v1_relat_1(C))),
% 2.23/0.80 inference(miniscoping,[status(thm)],[f60])).
% 2.23/0.80 fof(f62,plain,(
% 2.23/0.80 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))|v1_relat_1(X0))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f61])).
% 2.23/0.80 fof(f63,plain,(
% 2.23/0.80 ![A,B,C]: (~m2_relset_1(C,A,B)|(((B=k1_xboole_0&~A=k1_xboole_0)|(v1_funct_2(C,A,B)<=>A=k4_relset_1(A,B,C)))&(~B=k1_xboole_0|(A=k1_xboole_0|(v1_funct_2(C,A,B)<=>C=k1_xboole_0)))))),
% 2.23/0.80 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 2.23/0.80 fof(f64,definition,(
% 2.23/0.80 ![A,B]: (sP0_prd(B,A)<=>(B=k1_xboole_0&~A=k1_xboole_0))),
% 2.23/0.80 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 2.23/0.80 fof(f65,plain,(
% 2.23/0.80 ![A,B,C]: (~m2_relset_1(C,A,B)|((sP0_prd(B,A)|(v1_funct_2(C,A,B)<=>A=k4_relset_1(A,B,C)))&(~B=k1_xboole_0|(A=k1_xboole_0|(v1_funct_2(C,A,B)<=>C=k1_xboole_0)))))),
% 2.23/0.80 inference(formula_renaming,[status(thm)],[f63,f64])).
% 2.23/0.80 fof(f66,plain,(
% 2.23/0.80 ![A,B,C]: (~m2_relset_1(C,A,B)|((sP0_prd(B,A)|((~v1_funct_2(C,A,B)|A=k4_relset_1(A,B,C))&(v1_funct_2(C,A,B)|~A=k4_relset_1(A,B,C))))&(~B=k1_xboole_0|(A=k1_xboole_0|((~v1_funct_2(C,A,B)|C=k1_xboole_0)&(v1_funct_2(C,A,B)|~C=k1_xboole_0))))))),
% 2.23/0.80 inference(NNF_transformation,[status(thm)],[f65])).
% 2.23/0.80 fof(f68,plain,(
% 2.23/0.80 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|sP0_prd(X2,X1)|v1_funct_2(X0,X1,X2)|~X1=k4_relset_1(X1,X2,X0))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f66])).
% 2.23/0.80 fof(f71,plain,(
% 2.23/0.80 ![A,B]: (~v1_relat_1(B)|(![C]: ((~v1_relat_1(C)|~v1_funct_1(C))|(C=k5_relset_2(A,B)<=>(k1_relat_1(C)=k1_zfmisc_1(A)&(![D]: (~r1_tarski(D,A)|k1_funct_1(C,D)=k9_relat_1(B,D))))))))),
% 2.23/0.80 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 2.23/0.80 fof(f72,plain,(
% 2.23/0.80 ![A,B]: (~v1_relat_1(B)|(![C]: ((~v1_relat_1(C)|~v1_funct_1(C))|((~C=k5_relset_2(A,B)|(k1_relat_1(C)=k1_zfmisc_1(A)&(![D]: (~r1_tarski(D,A)|k1_funct_1(C,D)=k9_relat_1(B,D)))))&(C=k5_relset_2(A,B)|(~k1_relat_1(C)=k1_zfmisc_1(A)|(?[D]: (r1_tarski(D,A)&~k1_funct_1(C,D)=k9_relat_1(B,D)))))))))),
% 2.23/0.80 inference(NNF_transformation,[status(thm)],[f71])).
% 2.23/0.80 fof(f73,plain,(
% 2.23/0.80 ![B]: (~v1_relat_1(B)|(![C]: ((~v1_relat_1(C)|~v1_funct_1(C))|((![A]: (~C=k5_relset_2(A,B)|(k1_relat_1(C)=k1_zfmisc_1(A)&(![D]: (~r1_tarski(D,A)|k1_funct_1(C,D)=k9_relat_1(B,D))))))&(![A]: (C=k5_relset_2(A,B)|(~k1_relat_1(C)=k1_zfmisc_1(A)|(?[D]: (r1_tarski(D,A)&~k1_funct_1(C,D)=k9_relat_1(B,D))))))))))),
% 2.23/0.80 inference(miniscoping,[status(thm)],[f72])).
% 2.23/0.80 fof(f74,plain,(
% 2.23/0.80 ![B]: (~v1_relat_1(B)|(![C]: ((~v1_relat_1(C)|~v1_funct_1(C))|((![A]: (~C=k5_relset_2(A,B)|(k1_relat_1(C)=k1_zfmisc_1(A)&(![D]: (~r1_tarski(D,A)|k1_funct_1(C,D)=k9_relat_1(B,D))))))&(![A]: (C=k5_relset_2(A,B)|(~k1_relat_1(C)=k1_zfmisc_1(A)|(r1_tarski(sK3_skl(A,C,B),A)&~k1_funct_1(C,sK3_skl(A,C,B))=k9_relat_1(B,sK3_skl(A,C,B))))))))))),
% 2.23/0.80 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(D,sK3_skl(A,C,B))],[f73])).
% 2.23/0.80 fof(f75,plain,(
% 2.23/0.80 ![X0,X1,X2]: (~v1_relat_1(X0)|~v1_relat_1(X1)|~v1_funct_1(X1)|~X1=k5_relset_2(X2,X0)|k1_relat_1(X1)=k1_zfmisc_1(X2))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f74])).
% 2.23/0.80 fof(f81,plain,(
% 2.23/0.80 ![A,B]: (~v1_relat_1(B)|(v1_relat_1(k5_relset_2(A,B))&v1_funct_1(k5_relset_2(A,B))))),
% 2.23/0.80 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 2.23/0.80 fof(f82,plain,(
% 2.23/0.80 ![B]: (~v1_relat_1(B)|((![A]: v1_relat_1(k5_relset_2(A,B)))&(![A]: v1_funct_1(k5_relset_2(A,B)))))),
% 2.23/0.80 inference(miniscoping,[status(thm)],[f81])).
% 2.23/0.80 fof(f83,plain,(
% 2.23/0.80 ![X0,X1]: (~v1_relat_1(X0)|v1_relat_1(k5_relset_2(X1,X0)))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f82])).
% 2.23/0.80 fof(f84,plain,(
% 2.23/0.80 ![X0,X1]: (~v1_relat_1(X0)|v1_funct_1(k5_relset_2(X1,X0)))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f82])).
% 2.23/0.80 fof(f85,plain,(
% 2.23/0.80 ![A,B,C]: (~m2_relset_1(C,A,B)|m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))))),
% 2.23/0.80 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 2.23/0.80 fof(f86,plain,(
% 2.23/0.80 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f85])).
% 2.23/0.80 fof(f96,plain,(
% 2.23/0.80 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f24])).
% 2.23/0.80 fof(f112,plain,(
% 2.23/0.80 (v1_xboole_0(sK7_skl)&v1_relat_1(sK7_skl))),
% 2.23/0.80 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(A,sK7_skl)],[f32])).
% 2.23/0.80 fof(f113,plain,(
% 2.23/0.80 v1_xboole_0(sK7_skl)),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f112])).
% 2.23/0.80 fof(f132,plain,(
% 2.23/0.80 ![A,B,C]: (~m1_relset_1(C,A,B)|k4_relset_1(A,B,C)=k1_relat_1(C))),
% 2.23/0.80 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 2.23/0.80 fof(f133,plain,(
% 2.23/0.80 ![X0,X1,X2]: (~m1_relset_1(X0,X1,X2)|k4_relset_1(X1,X2,X0)=k1_relat_1(X0))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f132])).
% 2.23/0.80 fof(f134,plain,(
% 2.23/0.80 ![A,B,C]: ((~m2_relset_1(C,A,B)|m1_relset_1(C,A,B))&(m2_relset_1(C,A,B)|~m1_relset_1(C,A,B)))),
% 2.23/0.80 inference(NNF_transformation,[status(thm)],[f39])).
% 2.23/0.80 fof(f135,plain,(
% 2.23/0.80 (![A,B,C]: (~m2_relset_1(C,A,B)|m1_relset_1(C,A,B)))&(![A,B,C]: (m2_relset_1(C,A,B)|~m1_relset_1(C,A,B)))),
% 2.23/0.80 inference(miniscoping,[status(thm)],[f134])).
% 2.23/0.80 fof(f136,plain,(
% 2.23/0.80 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f135])).
% 2.23/0.80 fof(f138,plain,(
% 2.23/0.80 ![A]: r1_tarski(A,A)),
% 2.23/0.80 inference(miniscoping,[status(thm)],[f40])).
% 2.23/0.80 fof(f139,plain,(
% 2.23/0.80 ![X0]: (r1_tarski(X0,X0))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f138])).
% 2.23/0.80 fof(f140,plain,(
% 2.23/0.80 ![A,B,C]: (~v1_relat_1(C)|((~r1_tarski(k1_relat_1(C),A)|~r1_tarski(k2_relat_1(C),B))|m2_relset_1(C,A,B)))),
% 2.23/0.80 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 2.23/0.80 fof(f141,plain,(
% 2.23/0.80 ![C]: (~v1_relat_1(C)|(![A,B]: ((~r1_tarski(k1_relat_1(C),A)|~r1_tarski(k2_relat_1(C),B))|m2_relset_1(C,A,B))))),
% 2.23/0.80 inference(miniscoping,[status(thm)],[f140])).
% 2.23/0.80 fof(f142,plain,(
% 2.23/0.80 ![X0,X1,X2]: (~v1_relat_1(X0)|~r1_tarski(k1_relat_1(X0),X1)|~r1_tarski(k2_relat_1(X0),X2)|m2_relset_1(X0,X1,X2))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f141])).
% 2.23/0.80 fof(f145,plain,(
% 2.23/0.80 ![A,B,C]: (~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))|r1_tarski(k2_relat_1(k5_relset_2(A,C)),k1_zfmisc_1(k2_relat_1(C))))),
% 2.23/0.80 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 2.23/0.80 fof(f146,plain,(
% 2.23/0.80 ![A,C]: ((![B]: ~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))))|r1_tarski(k2_relat_1(k5_relset_2(A,C)),k1_zfmisc_1(k2_relat_1(C))))),
% 2.23/0.80 inference(miniscoping,[status(thm)],[f145])).
% 2.23/0.80 fof(f147,plain,(
% 2.23/0.80 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))|r1_tarski(k2_relat_1(k5_relset_2(X1,X0)),k1_zfmisc_1(k2_relat_1(X0))))),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f146])).
% 2.23/0.80 fof(f160,plain,(
% 2.23/0.80 ![A]: (~v1_xboole_0(A)|A=k1_xboole_0)),
% 2.23/0.80 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 2.23/0.80 fof(f161,plain,(
% 2.23/0.80 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f160])).
% 2.23/0.80 fof(f168,plain,(
% 2.23/0.80 ![A,B]: ((~sP0_prd(B,A)|(B=k1_xboole_0&~A=k1_xboole_0))&(sP0_prd(B,A)|(~B=k1_xboole_0|A=k1_xboole_0)))),
% 2.23/0.80 inference(NNF_transformation,[status(thm)],[f64])).
% 2.23/0.80 fof(f169,plain,(
% 2.23/0.80 (![A,B]: (~sP0_prd(B,A)|(B=k1_xboole_0&~A=k1_xboole_0)))&(![A,B]: (sP0_prd(B,A)|(~B=k1_xboole_0|A=k1_xboole_0)))),
% 2.23/0.80 inference(miniscoping,[status(thm)],[f168])).
% 2.23/0.80 fof(f170,plain,(
% 2.23/0.80 ![X0,X1]: (~sP0_prd(X0,X1)|X0=k1_xboole_0)),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f169])).
% 2.23/0.80 fof(f171,plain,(
% 2.23/0.80 ![X0,X1]: (~sP0_prd(X0,X1)|~X1=k1_xboole_0)),
% 2.23/0.80 inference(cnf_transformation,[status(thm)],[f169])).
% 2.23/0.80 fof(f173,definition,(
% 2.23/0.80 sQ0_spl <=> (v1_funct_1(k5_relset_2(sK0_skl,sK1_skl)))),
% 2.23/0.80 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 2.23/0.80 fof(f175,plain,(
% 2.23/0.80 ~v1_funct_1(k5_relset_2(sK0_skl,sK1_skl))|sQ0_spl),
% 2.23/0.80 inference(component_clause,[status(thm)],[f173])).
% 2.23/0.80 fof(f176,definition,(
% 2.23/0.80 sQ1_spl <=> (v1_funct_2(k5_relset_2(sK0_skl,sK1_skl),k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl))))),
% 2.23/0.80 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 2.23/0.80 fof(f179,definition,(
% 2.23/0.80 sQ2_spl <=> (m2_relset_1(k5_relset_2(sK0_skl,sK1_skl),k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl))))),
% 2.23/0.80 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 2.23/0.80 fof(f180,plain,(
% 2.23/0.80 m2_relset_1(k5_relset_2(sK0_skl,sK1_skl),k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)))|~sQ2_spl),
% 2.23/0.80 inference(component_clause,[status(thm)],[f179])).
% 2.23/0.80 fof(f181,plain,(
% 2.23/0.80 ~m2_relset_1(k5_relset_2(sK0_skl,sK1_skl),k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)))|sQ2_spl),
% 2.23/0.80 inference(component_clause,[status(thm)],[f179])).
% 2.23/0.80 fof(f182,plain,(
% 2.23/0.80 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 2.23/0.80 inference(split_clause,[status(thm)],[f55,f173,f176,f179])).
% 2.23/0.80 fof(f185,plain,(
% 2.23/0.80 ![X0,X1]: (~v1_relat_1(X0)|~v1_relat_1(k5_relset_2(X1,X0))|~v1_funct_1(k5_relset_2(X1,X0))|k1_relat_1(k5_relset_2(X1,X0))=k1_zfmisc_1(X1))),
% 2.23/0.80 inference(destructive_equality_resolution,[status(thm)],[f75])).
% 2.23/0.80 fof(f187,plain,(
% 2.23/0.80 ![X0]: (~sP0_prd(X0,k1_xboole_0))),
% 2.23/0.80 inference(destructive_equality_resolution,[status(thm)],[f171])).
% 2.23/0.80 fof(f189,plain,(
% 2.23/0.80 v1_relat_1(sK1_skl)),
% 2.23/0.80 inference(resolution,[status(thm)],[f62,f54])).
% 2.23/0.80 fof(f191,plain,(
% 2.23/0.80 ![X0,X1]: (~v1_relat_1(X0)|~v1_funct_1(k5_relset_2(X1,X0))|k1_relat_1(k5_relset_2(X1,X0))=k1_zfmisc_1(X1))),
% 2.23/0.80 inference(forward_subsumption_resolution,[status(thm)],[f185,f83])).
% 2.23/0.80 fof(f192,plain,(
% 2.23/0.80 ![X0,X1]: (~v1_relat_1(X0)|k1_relat_1(k5_relset_2(X1,X0))=k1_zfmisc_1(X1)|~v1_relat_1(X0))),
% 2.23/0.80 inference(resolution,[status(thm)],[f191,f84])).
% 2.23/0.80 fof(f193,plain,(
% 2.23/0.80 ![X0,X1]: (~v1_relat_1(X0)|k1_relat_1(k5_relset_2(X1,X0))=k1_zfmisc_1(X1))),
% 2.23/0.80 inference(duplicate_literals_removal,[status(thm)],[f192])).
% 2.23/0.80 fof(f194,plain,(
% 2.23/0.80 ![X0,X1]: (~v1_relat_1(X0)|~r1_tarski(k2_relat_1(X0),X1)|m2_relset_1(X0,k1_relat_1(X0),X1))),
% 2.23/0.80 inference(resolution,[status(thm)],[f139,f142])).
% 2.23/0.80 fof(f198,plain,(
% 2.23/0.80 ![X0]: (~v1_relat_1(X0)|m2_relset_1(X0,k1_relat_1(X0),k2_relat_1(X0)))),
% 2.23/0.80 inference(resolution,[status(thm)],[f194,f139])).
% 2.23/0.80 fof(f206,plain,(
% 2.23/0.80 ![X0]: (k1_relat_1(k5_relset_2(X0,sK1_skl))=k1_zfmisc_1(X0))),
% 2.23/0.80 inference(resolution,[status(thm)],[f193,f189])).
% 2.23/0.80 fof(f212,definition,(
% 2.23/0.80 sQ4_spl <=> (v1_relat_1(sK1_skl))),
% 2.23/0.80 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 2.23/0.80 fof(f214,plain,(
% 2.23/0.80 ~v1_relat_1(sK1_skl)|sQ4_spl),
% 2.23/0.80 inference(component_clause,[status(thm)],[f212])).
% 2.23/0.80 fof(f216,plain,(
% 2.23/0.80 $false|sQ4_spl),
% 2.23/0.80 inference(forward_subsumption_resolution,[status(thm)],[f214,f189])).
% 2.23/0.80 fof(f217,plain,(
% 2.23/0.80 sQ4_spl),
% 2.23/0.80 inference(contradiction_clause,[status(thm)],[f216])).
% 2.23/0.80 fof(f228,plain,(
% 2.23/0.80 ![X0]: (~v1_relat_1(k5_relset_2(X0,sK1_skl))|m2_relset_1(k5_relset_2(X0,sK1_skl),k1_zfmisc_1(X0),k2_relat_1(k5_relset_2(X0,sK1_skl))))),
% 2.23/0.80 inference(paramodulation,[status(thm)],[f206,f198])).
% 2.23/0.80 fof(f231,plain,(
% 2.23/0.80 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|v1_relat_1(X0))),
% 2.23/0.80 inference(resolution,[status(thm)],[f86,f62])).
% 2.23/0.80 fof(f233,plain,(
% 2.23/0.80 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))|~v1_relat_1(k5_relset_2(X1,X0))|m2_relset_1(k5_relset_2(X1,X0),k1_relat_1(k5_relset_2(X1,X0)),k1_zfmisc_1(k2_relat_1(X0))))),
% 2.23/0.80 inference(resolution,[status(thm)],[f147,f194])).
% 2.23/0.80 fof(f253,plain,(
% 2.23/0.80 ![X0]: (m2_relset_1(k5_relset_2(X0,sK1_skl),k1_zfmisc_1(X0),k2_relat_1(k5_relset_2(X0,sK1_skl)))|~v1_relat_1(sK1_skl))),
% 2.23/0.80 inference(resolution,[status(thm)],[f228,f83])).
% 2.23/0.80 fof(f254,definition,(
% 2.23/0.80 ![X0]: (sQ5_spl <=> (m2_relset_1(k5_relset_2(X0,sK1_skl),k1_zfmisc_1(X0),k2_relat_1(k5_relset_2(X0,sK1_skl)))))),
% 2.23/0.80 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 2.23/0.80 fof(f255,plain,(
% 2.23/0.80 ![X0]: (m2_relset_1(k5_relset_2(X0,sK1_skl),k1_zfmisc_1(X0),k2_relat_1(k5_relset_2(X0,sK1_skl)))|~sQ5_spl)),
% 2.23/0.80 inference(component_clause,[status(thm)],[f254])).
% 2.23/0.80 fof(f257,plain,(
% 2.23/0.80 sQ5_spl|~sQ4_spl),
% 2.23/0.80 inference(split_clause,[status(thm)],[f253,f254,f212])).
% 2.23/0.80 fof(f258,plain,(
% 2.23/0.80 ![X0]: (v1_relat_1(k5_relset_2(X0,sK1_skl))|~sQ5_spl)),
% 2.23/0.80 inference(resolution,[status(thm)],[f255,f231])).
% 2.23/0.80 fof(f286,plain,(
% 2.23/0.80 ![X0,X1]: (~m1_subset_1(sK1_skl,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))|m2_relset_1(k5_relset_2(X0,sK1_skl),k1_relat_1(k5_relset_2(X0,sK1_skl)),k1_zfmisc_1(k2_relat_1(sK1_skl)))|~sQ5_spl)),
% 2.23/0.80 inference(resolution,[status(thm)],[f233,f258])).
% 2.23/0.80 fof(f288,plain,(
% 2.23/0.80 ![X0,X1]: (~m1_subset_1(sK1_skl,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))|m2_relset_1(k5_relset_2(X0,sK1_skl),k1_zfmisc_1(X0),k1_zfmisc_1(k2_relat_1(sK1_skl)))|~sQ5_spl)),
% 2.23/0.80 inference(forward_demodulation,[status(thm)],[f206,f286])).
% 2.23/0.80 fof(f291,plain,(
% 2.23/0.80 sK7_skl=k1_xboole_0),
% 2.23/0.80 inference(resolution,[status(thm)],[f161,f113])).
% 2.23/0.80 fof(f296,plain,(
% 2.23/0.80 ![X0]: (~sP0_prd(X0,sK7_skl))),
% 2.23/0.80 inference(backward_demodulation,[status(thm)],[f291,f187])).
% 2.23/0.80 fof(f298,plain,(
% 2.23/0.80 ![X0,X1]: (~sP0_prd(X0,X1)|X0=sK7_skl)),
% 2.23/0.80 inference(backward_demodulation,[status(thm)],[f291,f170])).
% 2.23/0.80 fof(f342,plain,(
% 2.23/0.80 m2_relset_1(k5_relset_2(sK0_skl,sK1_skl),k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)))|~sQ5_spl),
% 2.23/0.80 inference(resolution,[status(thm)],[f288,f54])).
% 2.23/0.80 fof(f344,plain,(
% 2.23/0.80 $false|sQ2_spl|~sQ5_spl),
% 2.23/0.80 inference(forward_subsumption_resolution,[status(thm)],[f342,f181])).
% 2.23/0.80 fof(f345,plain,(
% 2.23/0.80 sQ2_spl|~sQ5_spl),
% 2.23/0.80 inference(contradiction_clause,[status(thm)],[f344])).
% 2.23/0.80 fof(f346,plain,(
% 2.23/0.80 ~v1_relat_1(sK1_skl)|sQ0_spl),
% 2.23/0.80 inference(resolution,[status(thm)],[f175,f84])).
% 2.23/0.80 fof(f347,plain,(
% 2.23/0.80 ~sQ4_spl|sQ0_spl),
% 2.23/0.80 inference(split_clause,[status(thm)],[f346,f212,f173])).
% 2.23/0.80 fof(f370,definition,(
% 2.23/0.80 sQ9_spl <=> (v1_xboole_0(sK7_skl))),
% 2.23/0.80 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 2.23/0.80 fof(f372,plain,(
% 2.23/0.80 ~v1_xboole_0(sK7_skl)|sQ9_spl),
% 2.23/0.80 inference(component_clause,[status(thm)],[f370])).
% 2.23/0.80 fof(f376,plain,(
% 2.23/0.80 $false|sQ9_spl),
% 2.23/0.80 inference(forward_subsumption_resolution,[status(thm)],[f372,f113])).
% 2.23/0.80 fof(f377,plain,(
% 2.23/0.80 sQ9_spl),
% 2.23/0.80 inference(contradiction_clause,[status(thm)],[f376])).
% 2.23/0.80 fof(f405,plain,(
% 2.23/0.80 sP0_prd(k1_zfmisc_1(k2_relat_1(sK1_skl)),k1_zfmisc_1(sK0_skl))|v1_funct_2(k5_relset_2(sK0_skl,sK1_skl),k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)))|~k1_zfmisc_1(sK0_skl)=k4_relset_1(k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)),k5_relset_2(sK0_skl,sK1_skl))|~sQ2_spl),
% 2.23/0.80 inference(resolution,[status(thm)],[f180,f68])).
% 2.23/0.80 fof(f407,definition,(
% 2.23/0.80 sQ12_spl <=> (sP0_prd(k1_zfmisc_1(k2_relat_1(sK1_skl)),k1_zfmisc_1(sK0_skl)))),
% 2.23/0.80 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 2.23/0.80 fof(f408,plain,(
% 2.23/0.80 sP0_prd(k1_zfmisc_1(k2_relat_1(sK1_skl)),k1_zfmisc_1(sK0_skl))|~sQ12_spl),
% 2.23/0.80 inference(component_clause,[status(thm)],[f407])).
% 2.23/0.80 fof(f410,definition,(
% 2.23/0.80 sQ13_spl <=> (k1_zfmisc_1(sK0_skl)=k4_relset_1(k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)),k5_relset_2(sK0_skl,sK1_skl)))),
% 2.23/0.80 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 2.23/0.80 fof(f412,plain,(
% 2.23/0.80 ~k1_zfmisc_1(sK0_skl)=k4_relset_1(k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)),k5_relset_2(sK0_skl,sK1_skl))|sQ13_spl),
% 2.23/0.80 inference(component_clause,[status(thm)],[f410])).
% 2.23/0.80 fof(f413,plain,(
% 2.23/0.80 sQ12_spl|sQ1_spl|~sQ13_spl|~sQ2_spl),
% 2.23/0.80 inference(split_clause,[status(thm)],[f405,f407,f176,f410,f179])).
% 2.23/0.80 fof(f428,definition,(
% 2.23/0.80 sQ16_spl <=> (sP0_prd(sK7_skl,sK7_skl))),
% 2.23/0.80 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 2.23/0.80 fof(f429,plain,(
% 2.23/0.80 sP0_prd(sK7_skl,sK7_skl)|~sQ16_spl),
% 2.23/0.80 inference(component_clause,[status(thm)],[f428])).
% 2.23/0.80 fof(f436,plain,(
% 2.23/0.80 $false|~sQ16_spl),
% 2.23/0.80 inference(forward_subsumption_resolution,[status(thm)],[f429,f296])).
% 2.23/0.80 fof(f437,plain,(
% 2.23/0.80 ~sQ16_spl),
% 2.23/0.80 inference(contradiction_clause,[status(thm)],[f436])).
% 2.23/0.80 fof(f460,plain,(
% 2.23/0.80 m1_relset_1(k5_relset_2(sK0_skl,sK1_skl),k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)))|~sQ2_spl),
% 2.23/0.80 inference(resolution,[status(thm)],[f136,f180])).
% 2.23/0.80 fof(f463,plain,(
% 2.23/0.80 k1_zfmisc_1(k2_relat_1(sK1_skl))=sK7_skl|~sQ12_spl),
% 2.23/0.80 inference(resolution,[status(thm)],[f408,f298])).
% 2.23/0.80 fof(f474,plain,(
% 2.23/0.81 ~v1_xboole_0(sK7_skl)|~sQ12_spl),
% 2.23/0.81 inference(paramodulation,[status(thm)],[f463,f96])).
% 2.23/0.81 fof(f482,plain,(
% 2.23/0.81 ~sQ9_spl|~sQ12_spl),
% 2.23/0.81 inference(split_clause,[status(thm)],[f474,f370,f407])).
% 2.23/0.81 fof(f564,definition,(
% 2.23/0.81 sQ24_spl <=> (v1_xboole_0(k1_zfmisc_1(k2_zfmisc_1(sK0_skl,sK2_skl))))),
% 2.23/0.81 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 2.23/0.81 fof(f565,plain,(
% 2.23/0.81 v1_xboole_0(k1_zfmisc_1(k2_zfmisc_1(sK0_skl,sK2_skl)))|~sQ24_spl),
% 2.23/0.81 inference(component_clause,[status(thm)],[f564])).
% 2.23/0.81 fof(f572,plain,(
% 2.23/0.81 $false|~sQ24_spl),
% 2.23/0.81 inference(forward_subsumption_resolution,[status(thm)],[f565,f96])).
% 2.23/0.81 fof(f573,plain,(
% 2.23/0.81 ~sQ24_spl),
% 2.23/0.81 inference(contradiction_clause,[status(thm)],[f572])).
% 2.23/0.81 fof(f583,plain,(
% 2.23/0.81 k4_relset_1(k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)),k5_relset_2(sK0_skl,sK1_skl))=k1_relat_1(k5_relset_2(sK0_skl,sK1_skl))|~sQ2_spl),
% 2.23/0.81 inference(resolution,[status(thm)],[f460,f133])).
% 2.23/0.81 fof(f585,plain,(
% 2.23/0.81 k4_relset_1(k1_zfmisc_1(sK0_skl),k1_zfmisc_1(k2_relat_1(sK1_skl)),k5_relset_2(sK0_skl,sK1_skl))=k1_zfmisc_1(sK0_skl)|~sQ2_spl),
% 2.23/0.81 inference(forward_demodulation,[status(thm)],[f206,f583])).
% 2.23/0.81 fof(f903,plain,(
% 2.23/0.81 $false|sQ13_spl|~sQ2_spl),
% 2.23/0.81 inference(forward_subsumption_resolution,[status(thm)],[f585,f412])).
% 2.23/0.81 fof(f904,plain,(
% 2.23/0.81 sQ13_spl|~sQ2_spl),
% 2.23/0.81 inference(contradiction_clause,[status(thm)],[f903])).
% 2.23/0.81 fof(f905,plain,(
% 2.23/0.81 $false),
% 2.23/0.81 inference(sat_refutation,[status(thm)],[f182,f217,f257,f345,f347,f377,f413,f437,f482,f573,f904])).
% 2.23/0.81 % SZS output end CNFRefutation for theBenchmark.p
% 2.23/0.82 % Elapsed time: 0.355518 seconds
% 2.23/0.82 % CPU time: 2.483206 seconds
% 2.23/0.82 % Total memory used: 117.715 MB
% 2.23/0.82 % Net memory used: 115.944 MB
%------------------------------------------------------------------------------