%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU427+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 29.27s 8.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU427+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n006.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 06:27:44 UTC 2026
% 0.18/0.43 % CPUTime :
% 4.55/4.82 % Drodi V4.1.1
% 29.27/8.06 % Refutation found
% 29.27/8.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 29.27/8.06 % SZS output start CNFRefutation for theBenchmark
% 29.27/8.06 fof(f25,axiom,(
% 29.27/8.06 (? [A] : v1_xboole_0(A) )),
% 29.27/8.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.27/8.06 fof(f33,axiom,(
% 29.27/8.06 (! [A] :( v1_xboole_0(A)<=> A = k1_xboole_0 ) )),
% 29.27/8.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.27/8.06 fof(f54,axiom,(
% 29.27/8.06 (! [A,B] : k2_xboole_0(A,B) = k2_xboole_0(B,A) )),
% 29.27/8.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.27/8.06 fof(f62,axiom,(
% 29.27/8.06 (! [A] : k2_xboole_0(A,k1_xboole_0) = A )),
% 29.27/8.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.27/8.06 fof(f570,axiom,(
% 29.27/8.06 (! [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) ) )),
% 29.27/8.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.27/8.06 fof(f19062,axiom,(
% 29.27/8.06 (! [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) ) )),
% 29.27/8.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.27/8.06 fof(f19094,axiom,(
% 29.27/8.06 (! [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 ) ) )) )),
% 29.27/8.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.27/8.06 fof(f19097,conjecture,(
% 29.27/8.06 (! [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) ) ) )) )) )),
% 29.27/8.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.27/8.06 fof(f19098,negated_conjecture,(
% 29.27/8.06 ~((! [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) ) ) )) )) ))),
% 29.27/8.06 inference(negated_conjecture,[status(cth)],[f19097])).
% 29.27/8.06 fof(f19178,plain,(
% 29.27/8.06 v1_xboole_0(sK20_skl)),
% 29.27/8.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f25])).
% 29.27/8.06 fof(f19179,plain,(
% 29.27/8.06 v1_xboole_0(sK20_skl)),
% 29.27/8.06 inference(cnf_transformation,[status(thm)],[f19178])).
% 29.27/8.06 fof(f19220,plain,(
% 29.27/8.06 ![A]: ((~v1_xboole_0(A)|A=k1_xboole_0)&(v1_xboole_0(A)|~A=k1_xboole_0))),
% 29.27/8.06 inference(NNF_transformation,[status(thm)],[f33])).
% 29.27/8.06 fof(f19221,plain,(
% 29.27/8.06 (![A]: (~v1_xboole_0(A)|A=k1_xboole_0))&(![A]: (v1_xboole_0(A)|~A=k1_xboole_0))),
% 29.27/8.06 inference(miniscoping,[status(thm)],[f19220])).
% 29.27/8.06 fof(f19222,plain,(
% 29.27/8.06 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 29.27/8.06 inference(cnf_transformation,[status(thm)],[f19221])).
% 29.27/8.06 fof(f19304,plain,(
% 29.27/8.06 ![X0,X1]: (k2_xboole_0(X0,X1)=k2_xboole_0(X1,X0))),
% 29.27/8.06 inference(cnf_transformation,[status(thm)],[f54])).
% 29.27/8.06 fof(f19311,plain,(
% 29.27/8.06 ![X0]: (k2_xboole_0(X0,k1_xboole_0)=X0)),
% 29.27/8.06 inference(cnf_transformation,[status(thm)],[f62])).
% 29.27/8.06 fof(f20317,plain,(
% 29.27/8.06 ![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))),
% 29.27/8.06 inference(pre_NNF_transformation,[status(thm)],[f570])).
% 29.27/8.06 fof(f20318,plain,(
% 29.27/8.06 ![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))),
% 29.27/8.06 inference(cnf_transformation,[status(thm)],[f20317])).
% 29.27/8.06 fof(f89208,plain,(
% 29.27/8.06 ![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))),
% 29.27/8.06 inference(pre_NNF_transformation,[status(thm)],[f19062])).
% 29.27/8.06 fof(f89209,plain,(
% 29.27/8.06 ![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))),
% 29.27/8.06 inference(cnf_transformation,[status(thm)],[f89208])).
% 29.27/8.06 fof(f89296,plain,(
% 29.27/8.06 ![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))))),
% 29.27/8.06 inference(pre_NNF_transformation,[status(thm)],[f19094])).
% 29.27/8.06 fof(f89297,plain,(
% 29.27/8.06 ![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)))))),
% 29.27/8.06 inference(NNF_transformation,[status(thm)],[f89296])).
% 29.27/8.06 fof(f89298,plain,(
% 29.27/8.06 ![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)))))),
% 29.27/8.06 inference(miniscoping,[status(thm)],[f89297])).
% 29.27/8.06 fof(f89299,plain,(
% 29.27/8.06 ![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)),
% 29.27/8.06 inference(cnf_transformation,[status(thm)],[f89298])).
% 29.27/8.06 fof(f89310,plain,(
% 29.27/8.06 (?[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))))))))),
% 29.27/8.06 inference(pre_NNF_transformation,[status(thm)],[f19098])).
% 29.27/8.06 fof(f89311,plain,(
% 29.27/8.06 ?[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)))))))),
% 29.27/8.06 inference(miniscoping,[status(thm)],[f89310])).
% 29.27/8.06 fof(f89312,plain,(
% 29.27/8.06 (m1_subset_1(sK6524_skl,k1_zfmisc_1(sK6523_skl))&(m1_subset_1(sK6525_skl,k1_zfmisc_1(sK6523_skl))&(m1_subset_1(sK6527_skl,k1_zfmisc_1(k2_zfmisc_1(sK6523_skl,sK6526_skl)))&(k4_relset_2(k1_zfmisc_1(sK6523_skl),sK6526_skl,k6_relset_2(sK6526_skl,sK6523_skl,sK6527_skl),k3_pua2mss1(sK6524_skl))=k1_xboole_0&~k8_relset_2(sK6523_skl,sK6526_skl,k4_subset_1(sK6523_skl,sK6524_skl,sK6525_skl),sK6527_skl)=k8_relset_2(sK6523_skl,sK6526_skl,sK6525_skl,sK6527_skl)))))),
% 29.27/8.06 inference(skolemize,[status(esa),new_symbols(skolem,[sK6523_skl,sK6524_skl,sK6525_skl,sK6526_skl,sK6527_skl]),skolemize(A,sK6523_skl),skolemize(C,sK6524_skl),skolemize(D,sK6525_skl),skolemize(B,sK6526_skl),skolemize(E,sK6527_skl)],[f89311])).
% 29.27/8.06 fof(f89313,plain,(
% 29.27/8.06 m1_subset_1(sK6524_skl,k1_zfmisc_1(sK6523_skl))),
% 29.27/8.06 inference(cnf_transformation,[status(thm)],[f89312])).
% 29.27/8.06 fof(f89314,plain,(
% 29.27/8.06 m1_subset_1(sK6525_skl,k1_zfmisc_1(sK6523_skl))),
% 29.27/8.06 inference(cnf_transformation,[status(thm)],[f89312])).
% 29.27/8.06 fof(f89315,plain,(
% 29.27/8.06 m1_subset_1(sK6527_skl,k1_zfmisc_1(k2_zfmisc_1(sK6523_skl,sK6526_skl)))),
% 29.27/8.06 inference(cnf_transformation,[status(thm)],[f89312])).
% 29.27/8.06 fof(f89316,plain,(
% 29.27/8.06 k4_relset_2(k1_zfmisc_1(sK6523_skl),sK6526_skl,k6_relset_2(sK6526_skl,sK6523_skl,sK6527_skl),k3_pua2mss1(sK6524_skl))=k1_xboole_0),
% 29.27/8.06 inference(cnf_transformation,[status(thm)],[f89312])).
% 29.27/8.06 fof(f89317,plain,(
% 29.27/8.06 ~k8_relset_2(sK6523_skl,sK6526_skl,k4_subset_1(sK6523_skl,sK6524_skl,sK6525_skl),sK6527_skl)=k8_relset_2(sK6523_skl,sK6526_skl,sK6525_skl,sK6527_skl)),
% 29.27/8.06 inference(cnf_transformation,[status(thm)],[f89312])).
% 29.27/8.06 fof(f100756,plain,(
% 29.27/8.06 sK20_skl=k1_xboole_0),
% 29.27/8.06 inference(resolution,[status(thm)],[f19179,f19222])).
% 29.27/8.06 fof(f100858,plain,(
% 29.27/8.06 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(sK6523_skl))|k4_subset_1(sK6523_skl,X0,sK6525_skl)=k2_xboole_0(X0,sK6525_skl))),
% 29.27/8.06 inference(resolution,[status(thm)],[f20318,f89314])).
% 29.27/8.06 fof(f100935,plain,(
% 29.27/8.06 k4_subset_1(sK6523_skl,sK6524_skl,sK6525_skl)=k2_xboole_0(sK6524_skl,sK6525_skl)),
% 29.27/8.06 inference(resolution,[status(thm)],[f100858,f89313])).
% 29.27/8.06 fof(f101143,plain,(
% 29.27/8.06 k4_relset_2(k1_zfmisc_1(sK6523_skl),sK6526_skl,k6_relset_2(sK6526_skl,sK6523_skl,sK6527_skl),k3_pua2mss1(sK6524_skl))=sK20_skl),
% 29.27/8.06 inference(backward_demodulation,[status(thm)],[f100756,f89316])).
% 29.27/8.06 fof(f101381,plain,(
% 29.27/8.06 k6_relset_2(sK6526_skl,sK6523_skl,sK6527_skl)=k5_relset_2(sK6523_skl,sK6527_skl)),
% 29.27/8.06 inference(resolution,[status(thm)],[f89209,f89315])).
% 29.27/8.06 fof(f101418,plain,(
% 18.88/8.58 k4_relset_2(k1_zfmisc_1(sK6523_skl),sK6526_skl,k5_relset_2(sK6523_skl,sK6527_skl),k3_pua2mss1(sK6524_skl))=sK20_skl),
% 18.88/8.58 inference(backward_demodulation,[status(thm)],[f101381,f101143])).
% 18.88/8.58 fof(f101724,plain,(
% 18.88/8.58 ![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)),
% 18.88/8.58 inference(forward_demodulation,[status(thm)],[f100756,f89299])).
% 18.88/8.58 fof(f101725,plain,(
% 18.88/8.58 ![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)),
% 18.88/8.58 inference(forward_demodulation,[status(thm)],[f100756,f101724])).
% 18.88/8.58 fof(f101727,plain,(
% 18.88/8.58 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(sK6523_skl))|~k4_relset_2(k1_zfmisc_1(sK6523_skl),sK6526_skl,k6_relset_2(sK6526_skl,sK6523_skl,sK6527_skl),k3_pua2mss1(X0))=sK20_skl|X0=sK20_skl)),
% 18.88/8.58 inference(resolution,[status(thm)],[f101725,f89315])).
% 18.88/8.58 fof(f101728,plain,(
% 18.88/8.58 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(sK6523_skl))|~k4_relset_2(k1_zfmisc_1(sK6523_skl),sK6526_skl,k5_relset_2(sK6523_skl,sK6527_skl),k3_pua2mss1(X0))=sK20_skl|X0=sK20_skl)),
% 18.88/8.58 inference(forward_demodulation,[status(thm)],[f101381,f101727])).
% 18.88/8.58 fof(f101788,plain,(
% 18.88/8.58 ~k8_relset_2(sK6523_skl,sK6526_skl,k2_xboole_0(sK6524_skl,sK6525_skl),sK6527_skl)=k8_relset_2(sK6523_skl,sK6526_skl,sK6525_skl,sK6527_skl)),
% 18.88/8.58 inference(backward_demodulation,[status(thm)],[f100935,f89317])).
% 18.88/8.58 fof(f101849,plain,(
% 18.88/8.58 ~k4_relset_2(k1_zfmisc_1(sK6523_skl),sK6526_skl,k5_relset_2(sK6523_skl,sK6527_skl),k3_pua2mss1(sK6524_skl))=sK20_skl|sK6524_skl=sK20_skl),
% 18.88/8.58 inference(resolution,[status(thm)],[f101728,f89313])).
% 18.88/8.58 fof(f101850,plain,(
% 18.88/8.58 ~sK20_skl=sK20_skl|sK6524_skl=sK20_skl),
% 18.88/8.58 inference(forward_demodulation,[status(thm)],[f101418,f101849])).
% 18.88/8.58 fof(f101851,plain,(
% 18.88/8.58 sK6524_skl=sK20_skl),
% 18.88/8.58 inference(trivial_equality_resolution,[status(thm)],[f101850])).
% 18.88/8.58 fof(f101856,plain,(
% 18.88/8.58 ~k8_relset_2(sK6523_skl,sK6526_skl,k2_xboole_0(sK20_skl,sK6525_skl),sK6527_skl)=k8_relset_2(sK6523_skl,sK6526_skl,sK6525_skl,sK6527_skl)),
% 18.88/8.58 inference(backward_demodulation,[status(thm)],[f101851,f101788])).
% 18.88/8.58 fof(f101955,plain,(
% 18.88/8.58 ![X0]: (k2_xboole_0(X0,sK20_skl)=X0)),
% 18.88/8.58 inference(forward_demodulation,[status(thm)],[f100756,f19311])).
% 18.88/8.58 fof(f101957,plain,(
% 18.88/8.58 ![X0]: (k2_xboole_0(sK20_skl,X0)=X0)),
% 18.88/8.58 inference(paramodulation,[status(thm)],[f19304,f101955])).
% 18.88/8.58 fof(f102334,plain,(
% 18.88/8.58 ~k8_relset_2(sK6523_skl,sK6526_skl,sK6525_skl,sK6527_skl)=k8_relset_2(sK6523_skl,sK6526_skl,sK6525_skl,sK6527_skl)),
% 18.88/8.58 inference(backward_demodulation,[status(thm)],[f101957,f101856])).
% 18.88/8.58 fof(f102359,plain,(
% 18.88/8.58 $false),
% 18.88/8.58 inference(trivial_equality_resolution,[status(thm)],[f102334])).
% 18.88/8.58 % SZS output end CNFRefutation for theBenchmark.p
% 5.36/8.71 % Elapsed time: 8.155889 seconds
% 5.36/8.71 % CPU time: 30.305225 seconds
% 5.36/8.71 % Total memory used: 5.335 GB
% 5.36/8.71 % Net memory used: 5.293 GB
%------------------------------------------------------------------------------