%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU427+2 : 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 : n014.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 16.90s 2.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU427+2 : 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.17/0.42 % Computer : n014.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 06:27:22 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.42/0.68 % Drodi V4.1.1
% 16.90/2.86 % Refutation found
% 16.90/2.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.90/2.86 % SZS output start CNFRefutation for theBenchmark
% 16.90/2.86 fof(f81,axiom,(
% 16.90/2.86 (! [A,B] :( r1_tarski(A,B)=> k2_xboole_0(A,B) = B ) )),
% 16.90/2.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.90/2.86 fof(f349,axiom,(
% 16.90/2.86 (! [A] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(A)) )),
% 16.90/2.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.90/2.86 fof(f433,axiom,(
% 16.90/2.86 (! [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) ) )),
% 16.90/2.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.90/2.86 fof(f540,axiom,(
% 16.90/2.86 ((! [A,B] :( m1_subset_1(A,k1_zfmisc_1(B))<=> r1_tarski(A,B) ) ))),
% 16.90/2.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.90/2.86 fof(f2485,axiom,(
% 16.90/2.86 np__0 = k1_xboole_0 ),
% 16.90/2.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.90/2.86 fof(f4463,axiom,(
% 16.90/2.86 (! [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) ) )),
% 16.90/2.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.90/2.86 fof(f4495,axiom,(
% 16.90/2.86 (! [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 ) ) )) )),
% 16.90/2.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.90/2.86 fof(f4498,conjecture,(
% 16.90/2.86 (! [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) ) ) )) )) )),
% 16.90/2.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.90/2.86 fof(f4499,negated_conjecture,(
% 16.90/2.86 ~((! [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) ) ) )) )) ))),
% 16.90/2.86 inference(negated_conjecture,[status(cth)],[f4498])).
% 16.90/2.86 fof(f4746,plain,(
% 16.90/2.86 ![A,B]: (~r1_tarski(A,B)|k2_xboole_0(A,B)=B)),
% 16.90/2.86 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 16.90/2.86 fof(f4747,plain,(
% 16.90/2.86 ![X0,X1]: (~r1_tarski(X0,X1)|k2_xboole_0(X0,X1)=X1)),
% 16.90/2.86 inference(cnf_transformation,[status(thm)],[f4746])).
% 16.90/2.86 fof(f5356,plain,(
% 16.90/2.86 ![X0]: (m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)))),
% 16.90/2.86 inference(cnf_transformation,[status(thm)],[f349])).
% 16.90/2.86 fof(f5582,plain,(
% 16.90/2.86 ![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))),
% 16.90/2.86 inference(pre_NNF_transformation,[status(thm)],[f433])).
% 16.90/2.86 fof(f5583,plain,(
% 16.90/2.86 ![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))),
% 16.90/2.86 inference(cnf_transformation,[status(thm)],[f5582])).
% 16.90/2.86 fof(f5830,plain,(
% 16.90/2.86 ![A,B]: ((~m1_subset_1(A,k1_zfmisc_1(B))|r1_tarski(A,B))&(m1_subset_1(A,k1_zfmisc_1(B))|~r1_tarski(A,B)))),
% 16.90/2.86 inference(NNF_transformation,[status(thm)],[f540])).
% 16.90/2.86 fof(f5831,plain,(
% 16.90/2.86 (![A,B]: (~m1_subset_1(A,k1_zfmisc_1(B))|r1_tarski(A,B)))&(![A,B]: (m1_subset_1(A,k1_zfmisc_1(B))|~r1_tarski(A,B)))),
% 16.90/2.86 inference(miniscoping,[status(thm)],[f5830])).
% 16.90/2.86 fof(f5832,plain,(
% 16.90/2.86 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|r1_tarski(X0,X1))),
% 16.90/2.86 inference(cnf_transformation,[status(thm)],[f5831])).
% 16.90/2.86 fof(f11703,plain,(
% 16.90/2.86 np__0=k1_xboole_0),
% 16.90/2.86 inference(cnf_transformation,[status(thm)],[f2485])).
% 16.90/2.86 fof(f17487,plain,(
% 16.90/2.86 ![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))),
% 16.90/2.86 inference(pre_NNF_transformation,[status(thm)],[f4463])).
% 16.90/2.86 fof(f17488,plain,(
% 16.90/2.86 ![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))),
% 16.90/2.86 inference(cnf_transformation,[status(thm)],[f17487])).
% 16.90/2.86 fof(f17575,plain,(
% 16.90/2.86 ![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))))),
% 16.90/2.86 inference(pre_NNF_transformation,[status(thm)],[f4495])).
% 16.90/2.86 fof(f17576,plain,(
% 16.90/2.86 ![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)))))),
% 16.90/2.86 inference(NNF_transformation,[status(thm)],[f17575])).
% 16.90/2.86 fof(f17577,plain,(
% 16.90/2.86 ![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)))))),
% 16.90/2.86 inference(miniscoping,[status(thm)],[f17576])).
% 16.90/2.86 fof(f17578,plain,(
% 16.90/2.86 ![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)),
% 16.90/2.86 inference(cnf_transformation,[status(thm)],[f17577])).
% 16.90/2.86 fof(f17589,plain,(
% 16.90/2.86 (?[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))))))))),
% 16.90/2.86 inference(pre_NNF_transformation,[status(thm)],[f4499])).
% 16.90/2.86 fof(f17590,plain,(
% 16.90/2.86 ?[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)))))))),
% 16.90/2.86 inference(miniscoping,[status(thm)],[f17589])).
% 16.90/2.86 fof(f17591,plain,(
% 16.90/2.86 (m1_subset_1(sK1207_skl,k1_zfmisc_1(sK1206_skl))&(m1_subset_1(sK1208_skl,k1_zfmisc_1(sK1206_skl))&(m1_subset_1(sK1210_skl,k1_zfmisc_1(k2_zfmisc_1(sK1206_skl,sK1209_skl)))&(k4_relset_2(k1_zfmisc_1(sK1206_skl),sK1209_skl,k6_relset_2(sK1209_skl,sK1206_skl,sK1210_skl),k3_pua2mss1(sK1207_skl))=k1_xboole_0&~k8_relset_2(sK1206_skl,sK1209_skl,k4_subset_1(sK1206_skl,sK1207_skl,sK1208_skl),sK1210_skl)=k8_relset_2(sK1206_skl,sK1209_skl,sK1208_skl,sK1210_skl)))))),
% 16.90/2.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK1206_skl,sK1207_skl,sK1208_skl,sK1209_skl,sK1210_skl]),skolemize(A,sK1206_skl),skolemize(C,sK1207_skl),skolemize(D,sK1208_skl),skolemize(B,sK1209_skl),skolemize(E,sK1210_skl)],[f17590])).
% 16.90/2.86 fof(f17592,plain,(
% 16.90/2.86 m1_subset_1(sK1207_skl,k1_zfmisc_1(sK1206_skl))),
% 16.90/2.86 inference(cnf_transformation,[status(thm)],[f17591])).
% 16.90/2.86 fof(f17593,plain,(
% 16.90/2.86 m1_subset_1(sK1208_skl,k1_zfmisc_1(sK1206_skl))),
% 16.90/2.86 inference(cnf_transformation,[status(thm)],[f17591])).
% 16.90/2.86 fof(f17594,plain,(
% 16.90/2.86 m1_subset_1(sK1210_skl,k1_zfmisc_1(k2_zfmisc_1(sK1206_skl,sK1209_skl)))),
% 16.90/2.86 inference(cnf_transformation,[status(thm)],[f17591])).
% 16.90/2.86 fof(f17595,plain,(
% 16.90/2.86 k4_relset_2(k1_zfmisc_1(sK1206_skl),sK1209_skl,k6_relset_2(sK1209_skl,sK1206_skl,sK1210_skl),k3_pua2mss1(sK1207_skl))=k1_xboole_0),
% 16.90/2.86 inference(cnf_transformation,[status(thm)],[f17591])).
% 16.90/2.86 fof(f17596,plain,(
% 16.90/2.86 ~k8_relset_2(sK1206_skl,sK1209_skl,k4_subset_1(sK1206_skl,sK1207_skl,sK1208_skl),sK1210_skl)=k8_relset_2(sK1206_skl,sK1209_skl,sK1208_skl,sK1210_skl)),
% 16.90/2.86 inference(cnf_transformation,[status(thm)],[f17591])).
% 16.90/2.86 fof(f19056,plain,(
% 16.90/2.86 ![X0]: (r1_tarski(k1_xboole_0,X0))),
% 16.90/2.86 inference(resolution,[status(thm)],[f5832,f5356])).
% 16.90/2.86 fof(f19479,plain,(
% 16.90/2.86 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|k4_subset_1(X1,k1_xboole_0,X0)=k2_xboole_0(k1_xboole_0,X0))),
% 16.90/2.86 inference(resolution,[status(thm)],[f5583,f5356])).
% 16.90/2.86 fof(f20736,plain,(
% 16.90/2.86 k6_relset_2(sK1209_skl,sK1206_skl,sK1210_skl)=k5_relset_2(sK1206_skl,sK1210_skl)),
% 16.90/2.86 inference(resolution,[status(thm)],[f17488,f17594])).
% 16.90/2.86 fof(f20793,plain,(
% 16.90/2.86 ![X0]: (r1_tarski(np__0,X0))),
% 16.90/2.86 inference(backward_demodulation,[status(thm)],[f11703,f19056])).
% 16.90/2.86 fof(f20811,plain,(
% 16.90/2.86 k4_relset_2(k1_zfmisc_1(sK1206_skl),sK1209_skl,k6_relset_2(sK1209_skl,sK1206_skl,sK1210_skl),k3_pua2mss1(sK1207_skl))=np__0),
% 16.90/2.86 inference(backward_demodulation,[status(thm)],[f11703,f17595])).
% 17.22/2.95 fof(f21621,plain,(
% 17.22/2.95 ![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))=np__0|X0=k1_xboole_0)),
% 17.22/2.95 inference(forward_demodulation,[status(thm)],[f11703,f17578])).
% 17.22/2.95 fof(f21622,plain,(
% 17.22/2.95 ![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))=np__0|X0=np__0)),
% 17.22/2.95 inference(forward_demodulation,[status(thm)],[f11703,f21621])).
% 17.22/2.95 fof(f21631,plain,(
% 17.22/2.95 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(sK1206_skl,X1)))|~k4_relset_2(k1_zfmisc_1(sK1206_skl),X1,k6_relset_2(X1,sK1206_skl,X0),k3_pua2mss1(sK1207_skl))=np__0|sK1207_skl=np__0)),
% 17.22/2.95 inference(resolution,[status(thm)],[f21622,f17592])).
% 17.22/2.95 fof(f28288,plain,(
% 17.22/2.95 ![X0]: (k2_xboole_0(np__0,X0)=X0)),
% 17.22/2.95 inference(resolution,[status(thm)],[f4747,f20793])).
% 17.22/2.95 fof(f30096,plain,(
% 17.22/2.95 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|k4_subset_1(X1,np__0,X0)=k2_xboole_0(k1_xboole_0,X0))),
% 17.22/2.95 inference(forward_demodulation,[status(thm)],[f11703,f19479])).
% 17.22/2.95 fof(f30097,plain,(
% 17.22/2.95 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|k4_subset_1(X1,np__0,X0)=k2_xboole_0(np__0,X0))),
% 17.22/2.95 inference(forward_demodulation,[status(thm)],[f11703,f30096])).
% 17.22/2.95 fof(f30098,plain,(
% 17.22/2.95 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|k4_subset_1(X1,np__0,X0)=X0)),
% 17.22/2.95 inference(forward_demodulation,[status(thm)],[f28288,f30097])).
% 17.22/2.95 fof(f30115,plain,(
% 17.22/2.95 k4_subset_1(sK1206_skl,np__0,sK1208_skl)=sK1208_skl),
% 17.22/2.95 inference(resolution,[status(thm)],[f30098,f17593])).
% 17.22/2.95 fof(f35760,plain,(
% 17.22/2.95 k4_relset_2(k1_zfmisc_1(sK1206_skl),sK1209_skl,k5_relset_2(sK1206_skl,sK1210_skl),k3_pua2mss1(sK1207_skl))=np__0),
% 17.22/2.95 inference(backward_demodulation,[status(thm)],[f20736,f20811])).
% 17.22/2.95 fof(f42218,plain,(
% 17.22/2.95 ~k4_relset_2(k1_zfmisc_1(sK1206_skl),sK1209_skl,k6_relset_2(sK1209_skl,sK1206_skl,sK1210_skl),k3_pua2mss1(sK1207_skl))=np__0|sK1207_skl=np__0),
% 17.22/2.95 inference(resolution,[status(thm)],[f21631,f17594])).
% 17.22/2.95 fof(f42225,plain,(
% 17.22/2.95 ~k4_relset_2(k1_zfmisc_1(sK1206_skl),sK1209_skl,k5_relset_2(sK1206_skl,sK1210_skl),k3_pua2mss1(sK1207_skl))=np__0|sK1207_skl=np__0),
% 17.22/2.95 inference(forward_demodulation,[status(thm)],[f20736,f42218])).
% 17.22/2.95 fof(f42226,plain,(
% 17.22/2.95 ~np__0=np__0|sK1207_skl=np__0),
% 17.22/2.95 inference(forward_demodulation,[status(thm)],[f35760,f42225])).
% 17.22/2.95 fof(f42227,plain,(
% 17.22/2.95 sK1207_skl=np__0),
% 17.22/2.95 inference(trivial_equality_resolution,[status(thm)],[f42226])).
% 17.22/2.95 fof(f42314,plain,(
% 17.22/2.95 ~k8_relset_2(sK1206_skl,sK1209_skl,k4_subset_1(sK1206_skl,np__0,sK1208_skl),sK1210_skl)=k8_relset_2(sK1206_skl,sK1209_skl,sK1208_skl,sK1210_skl)),
% 17.22/2.95 inference(backward_demodulation,[status(thm)],[f42227,f17596])).
% 17.22/2.95 fof(f42381,plain,(
% 17.22/2.95 ~k8_relset_2(sK1206_skl,sK1209_skl,sK1208_skl,sK1210_skl)=k8_relset_2(sK1206_skl,sK1209_skl,sK1208_skl,sK1210_skl)),
% 17.22/2.95 inference(forward_demodulation,[status(thm)],[f30115,f42314])).
% 17.22/2.95 fof(f42382,plain,(
% 17.22/2.95 $false),
% 17.22/2.95 inference(trivial_equality_resolution,[status(thm)],[f42381])).
% 17.22/2.95 % SZS output end CNFRefutation for theBenchmark.p
% 17.22/2.96 % Elapsed time: 2.520446 seconds
% 17.22/2.96 % CPU time: 17.642970 seconds
% 17.22/2.96 % Total memory used: 860.937 MB
% 17.22/2.96 % Net memory used: 833.170 MB
%------------------------------------------------------------------------------