%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU422+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 : n011.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 117.08s 15.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU422+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n011.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 06:25:56 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.66/1.03 % Drodi V4.1.1
% 117.08/15.86 % Refutation found
% 117.08/15.86 % SZS status Theorem for theBenchmark: Theorem is valid
% 117.08/15.86 % SZS output start CNFRefutation for theBenchmark
% 117.08/15.86 fof(f70,axiom,(
% 117.08/15.86 (! [A,B,C] :( ( r1_tarski(A,B)& r1_tarski(B,C) )=> r1_tarski(A,C) ) )),
% 117.08/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.08/15.86 fof(f185,axiom,(
% 117.08/15.86 (! [A,B] :( B = k1_zfmisc_1(A)<=> (! [C] :( r2_hidden(C,B)<=> r1_tarski(C,A) ) )) )),
% 117.08/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.08/15.86 fof(f267,axiom,(
% 117.08/15.86 (! [A,B] :( r1_tarski(A,B)=> r1_tarski(k1_zfmisc_1(A),k1_zfmisc_1(B)) ) )),
% 117.08/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.08/15.86 fof(f288,axiom,(
% 117.08/15.86 (! [A] : r1_tarski(A,k1_zfmisc_1(k3_tarski(A))) )),
% 117.08/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.08/15.86 fof(f334,axiom,(
% 117.08/15.86 (! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) )),
% 117.08/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.08/15.86 fof(f343,axiom,(
% 117.08/15.86 (! [A,B] :( ( ~ v1_xboole_0(A)=> ( m1_subset_1(B,A)<=> r2_hidden(B,A) ) )& ( v1_xboole_0(A)=> ( m1_subset_1(B,A)<=> v1_xboole_0(B) ) ) ) )),
% 117.08/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.08/15.86 fof(f540,axiom,(
% 117.08/15.86 ((! [A,B] :( m1_subset_1(A,k1_zfmisc_1(B))<=> r1_tarski(A,B) ) ))),
% 117.08/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.08/15.86 fof(f4486,axiom,(
% 117.08/15.86 (! [A] :( ~ v1_xboole_0(A)=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(A))=> B = k3_tarski(a_2_0_relset_2(A,B)) ) )) )),
% 117.08/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.08/15.86 fof(f4487,conjecture,(
% 117.08/15.86 (! [A] :( ~ v1_xboole_0(A)=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(A))=> m1_subset_1(a_2_0_relset_2(A,B),k1_zfmisc_1(k1_zfmisc_1(A))) ) )) )),
% 117.08/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 117.08/15.86 fof(f4488,negated_conjecture,(
% 117.08/15.86 ~((! [A] :( ~ v1_xboole_0(A)=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(A))=> m1_subset_1(a_2_0_relset_2(A,B),k1_zfmisc_1(k1_zfmisc_1(A))) ) )) ))),
% 117.08/15.86 inference(negated_conjecture,[status(cth)],[f4487])).
% 117.08/15.86 fof(f4714,plain,(
% 117.08/15.86 ![A,B,C]: ((~r1_tarski(A,B)|~r1_tarski(B,C))|r1_tarski(A,C))),
% 117.08/15.86 inference(pre_NNF_transformation,[status(thm)],[f70])).
% 117.08/15.86 fof(f4715,plain,(
% 117.08/15.86 ![A,C]: ((![B]: (~r1_tarski(A,B)|~r1_tarski(B,C)))|r1_tarski(A,C))),
% 117.08/15.86 inference(miniscoping,[status(thm)],[f4714])).
% 117.08/15.86 fof(f4716,plain,(
% 117.08/15.86 ![X0,X1,X2]: (~r1_tarski(X0,X1)|~r1_tarski(X1,X2)|r1_tarski(X0,X2))),
% 117.08/15.86 inference(cnf_transformation,[status(thm)],[f4715])).
% 117.08/15.86 fof(f4947,plain,(
% 117.08/15.86 ![A,B]: ((~B=k1_zfmisc_1(A)|(![C]: ((~r2_hidden(C,B)|r1_tarski(C,A))&(r2_hidden(C,B)|~r1_tarski(C,A)))))&(B=k1_zfmisc_1(A)|(?[C]: ((~r2_hidden(C,B)|~r1_tarski(C,A))&(r2_hidden(C,B)|r1_tarski(C,A))))))),
% 117.08/15.86 inference(NNF_transformation,[status(thm)],[f185])).
% 117.08/15.86 fof(f4948,plain,(
% 117.08/15.86 (![A,B]: (~B=k1_zfmisc_1(A)|((![C]: (~r2_hidden(C,B)|r1_tarski(C,A)))&(![C]: (r2_hidden(C,B)|~r1_tarski(C,A))))))&(![A,B]: (B=k1_zfmisc_1(A)|(?[C]: ((~r2_hidden(C,B)|~r1_tarski(C,A))&(r2_hidden(C,B)|r1_tarski(C,A))))))),
% 117.08/15.86 inference(miniscoping,[status(thm)],[f4947])).
% 117.08/15.86 fof(f4949,plain,(
% 117.08/15.86 (![A,B]: (~B=k1_zfmisc_1(A)|((![C]: (~r2_hidden(C,B)|r1_tarski(C,A)))&(![C]: (r2_hidden(C,B)|~r1_tarski(C,A))))))&(![A,B]: (B=k1_zfmisc_1(A)|((~r2_hidden(sK36_skl(B,A),B)|~r1_tarski(sK36_skl(B,A),A))&(r2_hidden(sK36_skl(B,A),B)|r1_tarski(sK36_skl(B,A),A)))))),
% 117.08/15.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl]),skolemize(C,sK36_skl(B,A))],[f4948])).
% 117.08/15.86 fof(f4950,plain,(
% 117.08/15.86 ![X0,X1,X2]: (~X0=k1_zfmisc_1(X1)|~r2_hidden(X2,X0)|r1_tarski(X2,X1))),
% 117.08/15.86 inference(cnf_transformation,[status(thm)],[f4949])).
% 117.08/15.86 fof(f5149,plain,(
% 117.08/15.86 ![A,B]: (~r1_tarski(A,B)|r1_tarski(k1_zfmisc_1(A),k1_zfmisc_1(B)))),
% 117.08/15.86 inference(pre_NNF_transformation,[status(thm)],[f267])).
% 117.08/15.86 fof(f5150,plain,(
% 117.08/15.86 ![X0,X1]: (~r1_tarski(X0,X1)|r1_tarski(k1_zfmisc_1(X0),k1_zfmisc_1(X1)))),
% 117.08/15.86 inference(cnf_transformation,[status(thm)],[f5149])).
% 117.08/15.86 fof(f5174,plain,(
% 117.08/15.86 ![X0]: (r1_tarski(X0,k1_zfmisc_1(k3_tarski(X0))))),
% 117.08/15.86 inference(cnf_transformation,[status(thm)],[f288])).
% 117.08/15.86 fof(f5320,plain,(
% 117.08/15.86 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 117.08/15.86 inference(cnf_transformation,[status(thm)],[f334])).
% 117.08/15.86 fof(f5336,plain,(
% 117.08/15.86 ![A,B]: ((v1_xboole_0(A)|(m1_subset_1(B,A)<=>r2_hidden(B,A)))&(~v1_xboole_0(A)|(m1_subset_1(B,A)<=>v1_xboole_0(B))))),
% 117.08/15.86 inference(pre_NNF_transformation,[status(thm)],[f343])).
% 117.08/15.86 fof(f5337,plain,(
% 117.08/15.86 ![A,B]: ((v1_xboole_0(A)|((~m1_subset_1(B,A)|r2_hidden(B,A))&(m1_subset_1(B,A)|~r2_hidden(B,A))))&(~v1_xboole_0(A)|((~m1_subset_1(B,A)|v1_xboole_0(B))&(m1_subset_1(B,A)|~v1_xboole_0(B)))))),
% 117.08/15.86 inference(NNF_transformation,[status(thm)],[f5336])).
% 117.08/15.86 fof(f5338,plain,(
% 117.08/15.86 (![A]: (v1_xboole_0(A)|((![B]: (~m1_subset_1(B,A)|r2_hidden(B,A)))&(![B]: (m1_subset_1(B,A)|~r2_hidden(B,A))))))&(![A]: (~v1_xboole_0(A)|((![B]: (~m1_subset_1(B,A)|v1_xboole_0(B)))&(![B]: (m1_subset_1(B,A)|~v1_xboole_0(B))))))),
% 117.08/15.86 inference(miniscoping,[status(thm)],[f5337])).
% 117.08/15.86 fof(f5339,plain,(
% 117.08/15.86 ![X0,X1]: (v1_xboole_0(X0)|~m1_subset_1(X1,X0)|r2_hidden(X1,X0))),
% 117.08/15.86 inference(cnf_transformation,[status(thm)],[f5338])).
% 117.08/15.86 fof(f5819,plain,(
% 117.08/15.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)))),
% 117.08/15.86 inference(NNF_transformation,[status(thm)],[f540])).
% 117.08/15.86 fof(f5820,plain,(
% 117.08/15.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)))),
% 117.08/15.86 inference(miniscoping,[status(thm)],[f5819])).
% 117.08/15.86 fof(f5822,plain,(
% 117.08/15.86 ![X0,X1]: (m1_subset_1(X0,k1_zfmisc_1(X1))|~r1_tarski(X0,X1))),
% 117.08/15.86 inference(cnf_transformation,[status(thm)],[f5820])).
% 117.08/15.86 fof(f17538,plain,(
% 117.08/15.86 ![A]: (v1_xboole_0(A)|(![B]: (~m1_subset_1(B,k1_zfmisc_1(A))|B=k3_tarski(a_2_0_relset_2(A,B)))))),
% 117.08/15.86 inference(pre_NNF_transformation,[status(thm)],[f4486])).
% 117.08/15.86 fof(f17539,plain,(
% 117.08/15.86 ![X0,X1]: (v1_xboole_0(X0)|~m1_subset_1(X1,k1_zfmisc_1(X0))|X1=k3_tarski(a_2_0_relset_2(X0,X1)))),
% 117.08/15.86 inference(cnf_transformation,[status(thm)],[f17538])).
% 117.08/15.86 fof(f17540,plain,(
% 117.08/15.86 (?[A]: (~v1_xboole_0(A)&(?[B]: (m1_subset_1(B,k1_zfmisc_1(A))&~m1_subset_1(a_2_0_relset_2(A,B),k1_zfmisc_1(k1_zfmisc_1(A)))))))),
% 117.08/15.86 inference(pre_NNF_transformation,[status(thm)],[f4488])).
% 117.08/15.86 fof(f17541,plain,(
% 117.08/15.86 (~v1_xboole_0(sK1205_skl)&(m1_subset_1(sK1206_skl,k1_zfmisc_1(sK1205_skl))&~m1_subset_1(a_2_0_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(k1_zfmisc_1(sK1205_skl)))))),
% 117.08/15.86 inference(skolemize,[status(esa),new_symbols(skolem,[sK1205_skl,sK1206_skl]),skolemize(A,sK1205_skl),skolemize(B,sK1206_skl)],[f17540])).
% 117.08/15.86 fof(f17542,plain,(
% 117.08/15.86 ~v1_xboole_0(sK1205_skl)),
% 117.08/15.86 inference(cnf_transformation,[status(thm)],[f17541])).
% 117.08/15.86 fof(f17543,plain,(
% 117.08/15.86 m1_subset_1(sK1206_skl,k1_zfmisc_1(sK1205_skl))),
% 117.08/15.86 inference(cnf_transformation,[status(thm)],[f17541])).
% 117.08/15.86 fof(f17544,plain,(
% 117.08/15.86 ~m1_subset_1(a_2_0_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(k1_zfmisc_1(sK1205_skl)))),
% 117.08/15.86 inference(cnf_transformation,[status(thm)],[f17541])).
% 117.08/15.86 fof(f18822,plain,(
% 117.08/15.86 ![X0,X1]: (~r2_hidden(X0,k1_zfmisc_1(X1))|r1_tarski(X0,X1))),
% 117.08/15.86 inference(destructive_equality_resolution,[status(thm)],[f4950])).
% 117.08/15.86 fof(f19844,plain,(
% 117.08/15.86 v1_xboole_0(k1_zfmisc_1(sK1205_skl))|r2_hidden(sK1206_skl,k1_zfmisc_1(sK1205_skl))),
% 117.08/15.86 inference(resolution,[status(thm)],[f5339,f17543])).
% 117.08/15.86 fof(f19845,plain,(
% 117.08/15.86 r2_hidden(sK1206_skl,k1_zfmisc_1(sK1205_skl))),
% 117.08/15.86 inference(forward_subsumption_resolution,[status(thm)],[f19844,f5320])).
% 117.08/15.86 fof(f19865,plain,(
% 117.08/15.86 r1_tarski(sK1206_skl,sK1205_skl)),
% 117.08/15.86 inference(resolution,[status(thm)],[f19845,f18822])).
% 117.08/15.86 fof(f19911,plain,(
% 117.08/15.86 ~r1_tarski(a_2_0_relset_2(sK1205_skl,sK1206_skl),k1_zfmisc_1(sK1205_skl))),
% 117.08/15.86 inference(resolution,[status(thm)],[f5822,f17544])).
% 117.08/15.86 fof(f19991,plain,(
% 117.08/15.86 v1_xboole_0(sK1205_skl)|sK1206_skl=k3_tarski(a_2_0_relset_2(sK1205_skl,sK1206_skl))),
% 117.08/15.86 inference(resolution,[status(thm)],[f17539,f17543])).
% 117.08/15.86 fof(f19995,plain,(
% 117.08/15.86 sK1206_skl=k3_tarski(a_2_0_relset_2(sK1205_skl,sK1206_skl))),
% 117.08/15.86 inference(forward_subsumption_resolution,[status(thm)],[f19991,f17542])).
% 117.08/15.86 fof(f21742,plain,(
% 117.08/15.86 ![X0]: (~r1_tarski(a_2_0_relset_2(sK1205_skl,sK1206_skl),X0)|~r1_tarski(X0,k1_zfmisc_1(sK1205_skl)))),
% 117.08/15.86 inference(resolution,[status(thm)],[f4716,f19911])).
% 117.08/15.86 fof(f42018,plain,(
% 117.08/15.86 ~r1_tarski(k1_zfmisc_1(k3_tarski(a_2_0_relset_2(sK1205_skl,sK1206_skl))),k1_zfmisc_1(sK1205_skl))),
% 117.08/15.86 inference(resolution,[status(thm)],[f5174,f21742])).
% 117.08/15.86 fof(f42048,plain,(
% 117.08/15.86 ~r1_tarski(k1_zfmisc_1(sK1206_skl),k1_zfmisc_1(sK1205_skl))),
% 117.08/15.86 inference(forward_demodulation,[status(thm)],[f19995,f42018])).
% 30.47/16.03 fof(f48052,plain,(
% 30.47/16.03 ~r1_tarski(sK1206_skl,sK1205_skl)),
% 30.47/16.03 inference(resolution,[status(thm)],[f42048,f5150])).
% 30.47/16.03 fof(f48060,plain,(
% 30.47/16.03 $false),
% 30.47/16.03 inference(forward_subsumption_resolution,[status(thm)],[f48052,f19865])).
% 30.47/16.03 % SZS output end CNFRefutation for theBenchmark.p
% 30.47/16.07 % Elapsed time: 15.602536 seconds
% 30.47/16.07 % CPU time: 118.491794 seconds
% 30.47/16.07 % Total memory used: 1.142 GB
% 30.47/16.07 % Net memory used: 1.070 GB
%------------------------------------------------------------------------------