%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU427+4 : 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:38 PM UTC 2026
% Result : Theorem 76.48s 23.19s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU427+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n001.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 06:33:39 UTC 2026
% 0.12/0.36 % CPUTime :
% 14.94/15.29 % Drodi V4.1.1
% 76.48/23.19 % Refutation found
% 76.48/23.19 % SZS status Theorem for theBenchmark: Theorem is valid
% 76.48/23.19 % SZS output start CNFRefutation for theBenchmark
% 76.48/23.19 fof(f25,axiom,(
% 76.48/23.19 (? [A] : v1_xboole_0(A) )),
% 76.48/23.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.48/23.19 fof(f33,axiom,(
% 76.48/23.19 (! [A] :( v1_xboole_0(A)<=> A = k1_xboole_0 ) )),
% 76.48/23.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.48/23.19 fof(f54,axiom,(
% 76.48/23.19 (! [A,B] : k2_xboole_0(A,B) = k2_xboole_0(B,A) )),
% 76.48/23.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.48/23.19 fof(f62,axiom,(
% 76.48/23.19 (! [A] : k2_xboole_0(A,k1_xboole_0) = A )),
% 76.48/23.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.48/23.19 fof(f486,axiom,(
% 76.48/23.19 (! [A] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)) )),
% 76.48/23.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.48/23.19 fof(f567,axiom,(
% 76.48/23.19 (! [A,B,C] :( ( m1_subset_1(B,k1_zfmisc_1(A))& m1_subset_1(C,k1_zfmisc_1(A)) )=> m1_subset_1(k4_subset_1(A,B,C),k1_zfmisc_1(A)) ) )),
% 76.48/23.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.48/23.19 fof(f569,axiom,(
% 76.48/23.19 (! [A,B,C] :( ( m1_subset_1(B,k1_zfmisc_1(A))& m1_subset_1(C,k1_zfmisc_1(A)) )=> k4_subset_1(A,B,B) = B ) )),
% 76.48/23.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.48/23.19 fof(f570,axiom,(
% 76.48/23.19 (! [A,B,C] :( ( m1_subset_1(B,k1_zfmisc_1(A))& m1_subset_1(C,k1_zfmisc_1(A)) )=> k4_subset_1(A,B,C) = k2_xboole_0(B,C) ) )),
% 76.48/23.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.48/23.19 fof(f71073,axiom,(
% 76.48/23.19 (! [A,B,C] :( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,A)))=> k6_relset_2(A,B,C) = k5_relset_2(B,C) ) )),
% 76.48/23.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.48/23.19 fof(f71105,axiom,(
% 76.48/23.19 (! [A,B,C] :( m1_subset_1(C,k1_zfmisc_1(A))=> (! [D] :( m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B)))=> ( k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,D),k3_pua2mss1(C)) = k1_xboole_0<=> C = k1_xboole_0 ) ) )) )),
% 76.48/23.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.48/23.19 fof(f71108,conjecture,(
% 76.48/23.19 (! [A,B,C] :( m1_subset_1(C,k1_zfmisc_1(A))=> (! [D] :( m1_subset_1(D,k1_zfmisc_1(A))=> (! [E] :( m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(A,B)))=> ( k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,E),k3_pua2mss1(C)) = k1_xboole_0=> k8_relset_2(A,B,k4_subset_1(A,C,D),E) = k8_relset_2(A,B,D,E) ) ) )) )) )),
% 76.48/23.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 76.48/23.19 fof(f71109,negated_conjecture,(
% 76.48/23.19 ~((! [A,B,C] :( m1_subset_1(C,k1_zfmisc_1(A))=> (! [D] :( m1_subset_1(D,k1_zfmisc_1(A))=> (! [E] :( m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(A,B)))=> ( k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,E),k3_pua2mss1(C)) = k1_xboole_0=> k8_relset_2(A,B,k4_subset_1(A,C,D),E) = k8_relset_2(A,B,D,E) ) ) )) )) ))),
% 76.48/23.19 inference(negated_conjecture,[status(cth)],[f71108])).
% 76.48/23.19 fof(f71189,plain,(
% 76.48/23.19 v1_xboole_0(sK20_skl)),
% 76.48/23.19 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f25])).
% 76.48/23.19 fof(f71190,plain,(
% 76.48/23.19 v1_xboole_0(sK20_skl)),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f71189])).
% 76.48/23.19 fof(f71231,plain,(
% 76.48/23.19 ![A]: ((~v1_xboole_0(A)|A=k1_xboole_0)&(v1_xboole_0(A)|~A=k1_xboole_0))),
% 76.48/23.19 inference(NNF_transformation,[status(thm)],[f33])).
% 76.48/23.19 fof(f71232,plain,(
% 76.48/23.19 (![A]: (~v1_xboole_0(A)|A=k1_xboole_0))&(![A]: (v1_xboole_0(A)|~A=k1_xboole_0))),
% 76.48/23.19 inference(miniscoping,[status(thm)],[f71231])).
% 76.48/23.19 fof(f71233,plain,(
% 76.48/23.19 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f71232])).
% 76.48/23.19 fof(f71315,plain,(
% 76.48/23.19 ![X0,X1]: (k2_xboole_0(X0,X1)=k2_xboole_0(X1,X0))),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f54])).
% 76.48/23.19 fof(f71322,plain,(
% 76.48/23.19 ![X0]: (k2_xboole_0(X0,k1_xboole_0)=X0)),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f62])).
% 76.48/23.19 fof(f72102,plain,(
% 76.48/23.19 ![X0]: (m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)))),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f486])).
% 76.48/23.19 fof(f72321,plain,(
% 76.48/23.19 ![A,B,C]: ((~m1_subset_1(B,k1_zfmisc_1(A))|~m1_subset_1(C,k1_zfmisc_1(A)))|m1_subset_1(k4_subset_1(A,B,C),k1_zfmisc_1(A)))),
% 76.48/23.19 inference(pre_NNF_transformation,[status(thm)],[f567])).
% 76.48/23.19 fof(f72322,plain,(
% 76.48/23.19 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|~m1_subset_1(X2,k1_zfmisc_1(X1))|m1_subset_1(k4_subset_1(X1,X0,X2),k1_zfmisc_1(X1)))),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f72321])).
% 76.48/23.19 fof(f72325,plain,(
% 76.48/23.19 ![A,B,C]: ((~m1_subset_1(B,k1_zfmisc_1(A))|~m1_subset_1(C,k1_zfmisc_1(A)))|k4_subset_1(A,B,B)=B)),
% 76.48/23.19 inference(pre_NNF_transformation,[status(thm)],[f569])).
% 76.48/23.19 fof(f72326,plain,(
% 76.48/23.19 ![A,B]: ((~m1_subset_1(B,k1_zfmisc_1(A))|(![C]: ~m1_subset_1(C,k1_zfmisc_1(A))))|k4_subset_1(A,B,B)=B)),
% 76.48/23.19 inference(miniscoping,[status(thm)],[f72325])).
% 76.48/23.19 fof(f72327,plain,(
% 76.48/23.19 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|~m1_subset_1(X2,k1_zfmisc_1(X1))|k4_subset_1(X1,X0,X0)=X0)),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f72326])).
% 76.48/23.19 fof(f72328,plain,(
% 76.48/23.19 ![A,B,C]: ((~m1_subset_1(B,k1_zfmisc_1(A))|~m1_subset_1(C,k1_zfmisc_1(A)))|k4_subset_1(A,B,C)=k2_xboole_0(B,C))),
% 76.48/23.19 inference(pre_NNF_transformation,[status(thm)],[f570])).
% 76.48/23.19 fof(f72329,plain,(
% 76.48/23.19 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|~m1_subset_1(X2,k1_zfmisc_1(X1))|k4_subset_1(X1,X0,X2)=k2_xboole_0(X0,X2))),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f72328])).
% 76.48/23.19 fof(f335911,plain,(
% 76.48/23.19 ![A,B,C]: (~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,A)))|k6_relset_2(A,B,C)=k5_relset_2(B,C))),
% 76.48/23.19 inference(pre_NNF_transformation,[status(thm)],[f71073])).
% 76.48/23.19 fof(f335912,plain,(
% 76.48/23.19 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))|k6_relset_2(X2,X1,X0)=k5_relset_2(X1,X0))),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f335911])).
% 76.48/23.19 fof(f335999,plain,(
% 76.48/23.19 ![A,B,C]: (~m1_subset_1(C,k1_zfmisc_1(A))|(![D]: (~m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B)))|(k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,D),k3_pua2mss1(C))=k1_xboole_0<=>C=k1_xboole_0))))),
% 76.48/23.19 inference(pre_NNF_transformation,[status(thm)],[f71105])).
% 76.48/23.19 fof(f336000,plain,(
% 76.48/23.19 ![A,B,C]: (~m1_subset_1(C,k1_zfmisc_1(A))|(![D]: (~m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B)))|((~k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,D),k3_pua2mss1(C))=k1_xboole_0|C=k1_xboole_0)&(k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,D),k3_pua2mss1(C))=k1_xboole_0|~C=k1_xboole_0)))))),
% 76.48/23.19 inference(NNF_transformation,[status(thm)],[f335999])).
% 76.48/23.19 fof(f336001,plain,(
% 76.48/23.19 ![A,C]: (~m1_subset_1(C,k1_zfmisc_1(A))|(![B,D]: (~m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B)))|((~k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,D),k3_pua2mss1(C))=k1_xboole_0|C=k1_xboole_0)&(k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,D),k3_pua2mss1(C))=k1_xboole_0|~C=k1_xboole_0)))))),
% 76.48/23.19 inference(miniscoping,[status(thm)],[f336000])).
% 76.48/23.19 fof(f336002,plain,(
% 76.48/23.19 ![X0,X1,X2,X3]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|~m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X3)))|~k4_relset_2(k1_zfmisc_1(X1),X3,k6_relset_2(X3,X1,X2),k3_pua2mss1(X0))=k1_xboole_0|X0=k1_xboole_0)),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f336001])).
% 76.48/23.19 fof(f336013,plain,(
% 76.48/23.19 (?[A,B,C]: (m1_subset_1(C,k1_zfmisc_1(A))&(?[D]: (m1_subset_1(D,k1_zfmisc_1(A))&(?[E]: (m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(A,B)))&(k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,E),k3_pua2mss1(C))=k1_xboole_0&~k8_relset_2(A,B,k4_subset_1(A,C,D),E)=k8_relset_2(A,B,D,E))))))))),
% 76.48/23.19 inference(pre_NNF_transformation,[status(thm)],[f71109])).
% 76.48/23.19 fof(f336014,plain,(
% 76.48/23.19 ?[A,C]: (m1_subset_1(C,k1_zfmisc_1(A))&(?[D]: (m1_subset_1(D,k1_zfmisc_1(A))&(?[B,E]: (m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(A,B)))&(k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,E),k3_pua2mss1(C))=k1_xboole_0&~k8_relset_2(A,B,k4_subset_1(A,C,D),E)=k8_relset_2(A,B,D,E)))))))),
% 76.48/23.19 inference(miniscoping,[status(thm)],[f336013])).
% 76.48/23.19 fof(f336015,plain,(
% 76.48/23.19 (m1_subset_1(sK23837_skl,k1_zfmisc_1(sK23836_skl))&(m1_subset_1(sK23838_skl,k1_zfmisc_1(sK23836_skl))&(m1_subset_1(sK23840_skl,k1_zfmisc_1(k2_zfmisc_1(sK23836_skl,sK23839_skl)))&(k4_relset_2(k1_zfmisc_1(sK23836_skl),sK23839_skl,k6_relset_2(sK23839_skl,sK23836_skl,sK23840_skl),k3_pua2mss1(sK23837_skl))=k1_xboole_0&~k8_relset_2(sK23836_skl,sK23839_skl,k4_subset_1(sK23836_skl,sK23837_skl,sK23838_skl),sK23840_skl)=k8_relset_2(sK23836_skl,sK23839_skl,sK23838_skl,sK23840_skl)))))),
% 76.48/23.19 inference(skolemize,[status(esa),new_symbols(skolem,[sK23836_skl,sK23837_skl,sK23838_skl,sK23839_skl,sK23840_skl]),skolemize(A,sK23836_skl),skolemize(C,sK23837_skl),skolemize(D,sK23838_skl),skolemize(B,sK23839_skl),skolemize(E,sK23840_skl)],[f336014])).
% 76.48/23.19 fof(f336016,plain,(
% 76.48/23.19 m1_subset_1(sK23837_skl,k1_zfmisc_1(sK23836_skl))),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f336015])).
% 76.48/23.19 fof(f336017,plain,(
% 76.48/23.19 m1_subset_1(sK23838_skl,k1_zfmisc_1(sK23836_skl))),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f336015])).
% 76.48/23.19 fof(f336018,plain,(
% 76.48/23.19 m1_subset_1(sK23840_skl,k1_zfmisc_1(k2_zfmisc_1(sK23836_skl,sK23839_skl)))),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f336015])).
% 76.48/23.19 fof(f336019,plain,(
% 76.48/23.19 k4_relset_2(k1_zfmisc_1(sK23836_skl),sK23839_skl,k6_relset_2(sK23839_skl,sK23836_skl,sK23840_skl),k3_pua2mss1(sK23837_skl))=k1_xboole_0),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f336015])).
% 76.48/23.19 fof(f336020,plain,(
% 76.48/23.19 ~k8_relset_2(sK23836_skl,sK23839_skl,k4_subset_1(sK23836_skl,sK23837_skl,sK23838_skl),sK23840_skl)=k8_relset_2(sK23836_skl,sK23839_skl,sK23838_skl,sK23840_skl)),
% 76.48/23.19 inference(cnf_transformation,[status(thm)],[f336015])).
% 76.48/23.19 fof(f370934,plain,(
% 76.48/23.19 sK20_skl=k1_xboole_0),
% 76.48/23.19 inference(resolution,[status(thm)],[f71190,f71233])).
% 76.48/23.19 fof(f371193,plain,(
% 76.48/23.19 ![X0]: (m1_subset_1(k4_subset_1(X0,k1_xboole_0,k1_xboole_0),k1_zfmisc_1(X0)))),
% 76.48/23.19 inference(resolution,[status(thm)],[f72322,f72102])).
% 76.48/23.19 fof(f371246,plain,(
% 76.48/23.19 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(sK23836_skl))|k4_subset_1(sK23836_skl,X0,X0)=X0)),
% 76.48/23.19 inference(resolution,[status(thm)],[f72327,f336017])).
% 76.48/23.19 fof(f371320,plain,(
% 76.48/23.19 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(sK23836_skl))|k4_subset_1(sK23836_skl,X0,sK23838_skl)=k2_xboole_0(X0,sK23838_skl))),
% 76.48/23.19 inference(resolution,[status(thm)],[f72329,f336017])).
% 76.48/23.19 fof(f373206,plain,(
% 76.48/23.19 k4_subset_1(sK23836_skl,k1_xboole_0,k1_xboole_0)=k1_xboole_0),
% 76.48/23.19 inference(resolution,[status(thm)],[f371246,f72102])).
% 76.48/23.19 fof(f374113,plain,(
% 76.48/23.19 ![X0]: (k2_xboole_0(X0,sK20_skl)=X0)),
% 76.48/23.19 inference(backward_demodulation,[status(thm)],[f370934,f71322])).
% 76.48/23.19 fof(f374114,plain,(
% 76.48/23.19 k4_subset_1(sK23836_skl,k1_xboole_0,k1_xboole_0)=sK20_skl),
% 76.48/23.19 inference(backward_demodulation,[status(thm)],[f370934,f373206])).
% 76.48/23.19 fof(f374170,plain,(
% 76.48/23.19 k4_relset_2(k1_zfmisc_1(sK23836_skl),sK23839_skl,k6_relset_2(sK23839_skl,sK23836_skl,sK23840_skl),k3_pua2mss1(sK23837_skl))=sK20_skl),
% 76.48/23.19 inference(backward_demodulation,[status(thm)],[f370934,f336019])).
% 76.48/23.19 fof(f374180,plain,(
% 76.48/23.19 k4_subset_1(sK23836_skl,sK20_skl,k1_xboole_0)=sK20_skl),
% 76.48/23.19 inference(forward_demodulation,[status(thm)],[f370934,f374114])).
% 76.48/23.19 fof(f374181,plain,(
% 76.48/23.19 k4_subset_1(sK23836_skl,sK20_skl,sK20_skl)=sK20_skl),
% 76.48/23.19 inference(forward_demodulation,[status(thm)],[f370934,f374180])).
% 76.48/23.19 fof(f374324,plain,(
% 76.48/23.19 k6_relset_2(sK23839_skl,sK23836_skl,sK23840_skl)=k5_relset_2(sK23836_skl,sK23840_skl)),
% 76.48/23.19 inference(resolution,[status(thm)],[f335912,f336018])).
% 76.48/23.19 fof(f375300,plain,(
% 76.48/23.19 ![X0,X1,X2,X3]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|~m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X3)))|~k4_relset_2(k1_zfmisc_1(X1),X3,k6_relset_2(X3,X1,X2),k3_pua2mss1(X0))=sK20_skl|X0=k1_xboole_0)),
% 76.48/23.19 inference(forward_demodulation,[status(thm)],[f370934,f336002])).
% 76.48/23.19 fof(f375301,plain,(
% 76.48/23.19 ![X0,X1,X2,X3]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|~m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X1,X3)))|~k4_relset_2(k1_zfmisc_1(X1),X3,k6_relset_2(X3,X1,X2),k3_pua2mss1(X0))=sK20_skl|X0=sK20_skl)),
% 76.48/23.19 inference(forward_demodulation,[status(thm)],[f370934,f375300])).
% 76.48/23.19 fof(f375306,plain,(
% 76.48/23.19 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK23836_skl,X1)))|~k4_relset_2(k1_zfmisc_1(sK23836_skl),X1,k6_relset_2(X1,sK23836_skl,X0),k3_pua2mss1(sK23837_skl))=sK20_skl|sK23837_skl=sK20_skl)),
% 76.48/23.19 inference(resolution,[status(thm)],[f375301,f336016])).
% 76.48/23.19 fof(f377275,plain,(
% 76.48/23.19 k4_relset_2(k1_zfmisc_1(sK23836_skl),sK23839_skl,k5_relset_2(sK23836_skl,sK23840_skl),k3_pua2mss1(sK23837_skl))=sK20_skl),
% 76.48/23.19 inference(backward_demodulation,[status(thm)],[f374324,f374170])).
% 76.48/23.19 fof(f378770,plain,(
% 76.48/23.19 ~k4_relset_2(k1_zfmisc_1(sK23836_skl),sK23839_skl,k6_relset_2(sK23839_skl,sK23836_skl,sK23840_skl),k3_pua2mss1(sK23837_skl))=sK20_skl|sK23837_skl=sK20_skl),
% 76.48/23.19 inference(resolution,[status(thm)],[f375306,f336018])).
% 76.48/23.19 fof(f378772,plain,(
% 76.48/23.19 ~k4_relset_2(k1_zfmisc_1(sK23836_skl),sK23839_skl,k5_relset_2(sK23836_skl,sK23840_skl),k3_pua2mss1(sK23837_skl))=sK20_skl|sK23837_skl=sK20_skl),
% 76.48/23.19 inference(forward_demodulation,[status(thm)],[f374324,f378770])).
% 23.90/24.94 fof(f378773,plain,(
% 23.90/24.94 ~sK20_skl=sK20_skl|sK23837_skl=sK20_skl),
% 23.90/24.94 inference(forward_demodulation,[status(thm)],[f377275,f378772])).
% 23.90/24.94 fof(f378774,plain,(
% 23.90/24.94 sK23837_skl=sK20_skl),
% 23.90/24.94 inference(trivial_equality_resolution,[status(thm)],[f378773])).
% 23.90/24.94 fof(f378792,plain,(
% 23.90/24.94 ~k8_relset_2(sK23836_skl,sK23839_skl,k4_subset_1(sK23836_skl,sK20_skl,sK23838_skl),sK23840_skl)=k8_relset_2(sK23836_skl,sK23839_skl,sK23838_skl,sK23840_skl)),
% 23.90/24.94 inference(backward_demodulation,[status(thm)],[f378774,f336020])).
% 23.90/24.94 fof(f381086,plain,(
% 23.90/24.94 ![X0]: (m1_subset_1(k4_subset_1(X0,sK20_skl,k1_xboole_0),k1_zfmisc_1(X0)))),
% 23.90/24.94 inference(forward_demodulation,[status(thm)],[f370934,f371193])).
% 23.90/24.94 fof(f381087,plain,(
% 23.90/24.94 ![X0]: (m1_subset_1(k4_subset_1(X0,sK20_skl,sK20_skl),k1_zfmisc_1(X0)))),
% 23.90/24.94 inference(forward_demodulation,[status(thm)],[f370934,f381086])).
% 23.90/24.94 fof(f381107,plain,(
% 23.90/24.94 k4_subset_1(sK23836_skl,k4_subset_1(sK23836_skl,sK20_skl,sK20_skl),sK23838_skl)=k2_xboole_0(k4_subset_1(sK23836_skl,sK20_skl,sK20_skl),sK23838_skl)),
% 23.90/24.94 inference(resolution,[status(thm)],[f381087,f371320])).
% 23.90/24.94 fof(f381182,plain,(
% 23.90/24.94 k4_subset_1(sK23836_skl,sK20_skl,sK23838_skl)=k2_xboole_0(k4_subset_1(sK23836_skl,sK20_skl,sK20_skl),sK23838_skl)),
% 23.90/24.94 inference(forward_demodulation,[status(thm)],[f374181,f381107])).
% 23.90/24.94 fof(f381183,plain,(
% 23.90/24.94 k4_subset_1(sK23836_skl,sK20_skl,sK23838_skl)=k2_xboole_0(sK23838_skl,k4_subset_1(sK23836_skl,sK20_skl,sK20_skl))),
% 23.90/24.94 inference(forward_demodulation,[status(thm)],[f71315,f381182])).
% 23.90/24.94 fof(f381184,plain,(
% 23.90/24.94 k4_subset_1(sK23836_skl,sK20_skl,sK23838_skl)=k2_xboole_0(sK23838_skl,sK20_skl)),
% 23.90/24.94 inference(forward_demodulation,[status(thm)],[f374181,f381183])).
% 23.90/24.94 fof(f381185,plain,(
% 23.90/24.94 k4_subset_1(sK23836_skl,sK20_skl,sK23838_skl)=sK23838_skl),
% 23.90/24.94 inference(forward_demodulation,[status(thm)],[f374113,f381184])).
% 23.90/24.94 fof(f383005,plain,(
% 23.90/24.94 ~k8_relset_2(sK23836_skl,sK23839_skl,sK23838_skl,sK23840_skl)=k8_relset_2(sK23836_skl,sK23839_skl,sK23838_skl,sK23840_skl)),
% 23.90/24.94 inference(backward_demodulation,[status(thm)],[f381185,f378792])).
% 23.90/24.94 fof(f383006,plain,(
% 23.90/24.94 $false),
% 23.90/24.94 inference(trivial_equality_resolution,[status(thm)],[f383005])).
% 23.90/24.94 % SZS output end CNFRefutation for theBenchmark.p
% 17.24/25.09 % Elapsed time: 24.063904 seconds
% 17.24/25.09 % CPU time: 79.145557 seconds
% 17.24/25.09 % Total memory used: 21.742 GB
% 17.24/25.09 % Net memory used: 21.590 GB
%------------------------------------------------------------------------------