%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU411+4 : 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 : n015.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:34 PM UTC 2026
% Result : Theorem 269.83s 46.30s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU411+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 06:25:58 UTC 2026
% 0.10/0.37 % CPUTime :
% 13.56/13.83 % Drodi V4.1.1
% 269.83/46.30 % Refutation found
% 269.83/46.30 % SZS status Theorem for theBenchmark: Theorem is valid
% 269.83/46.30 % SZS output start CNFRefutation for theBenchmark
% 269.83/46.30 fof(f31,axiom,(
% 269.83/46.30 (! [A,B,C] :( C = k3_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)& r2_hidden(D,B) ) ) )) )),
% 269.83/46.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 269.83/46.30 fof(f28604,axiom,(
% 269.83/46.30 (! [A] :( l1_orders_2(A)=> ( v1_lattice3(A)=> ~ v3_struct_0(A) ) ) )),
% 269.83/46.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 269.83/46.30 fof(f42238,axiom,(
% 269.83/46.30 (! [A] :( ( ~ v3_struct_0(A)& v4_orders_2(A)& v1_yellow_0(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v1_xboole_0(B)& v12_waybel_0(B,A)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> r2_hidden(k3_yellow_0(A),B) ) )) )),
% 269.83/46.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 269.83/46.30 fof(f66056,conjecture,(
% 269.83/46.30 (! [A] :( ( ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_yellow_0(A)& v1_lattice3(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v2_orders_2(B)& v3_orders_2(B)& v4_orders_2(B)& v1_yellow_0(B)& v1_lattice3(B)& l1_orders_2(B) )=> ( ( ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B))) )=> r2_hidden(k3_yellow_0(B),u1_struct_0(A)) ) ) )) )),
% 269.83/46.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 269.83/46.30 fof(f66057,negated_conjecture,(
% 269.83/46.30 ~((! [A] :( ( ~ v3_struct_0(A)& v2_orders_2(A)& v3_orders_2(A)& v4_orders_2(A)& v1_yellow_0(A)& v1_lattice3(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v2_orders_2(B)& v3_orders_2(B)& v4_orders_2(B)& v1_yellow_0(B)& v1_lattice3(B)& l1_orders_2(B) )=> ( ( ~ v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))& v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)& v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B)& m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B))) )=> r2_hidden(k3_yellow_0(B),u1_struct_0(A)) ) ) )) ))),
% 269.83/46.30 inference(negated_conjecture,[status(cth)],[f66056])).
% 269.83/46.30 fof(f66161,plain,(
% 269.83/46.30 ![A,B,C]: ((~C=k3_xboole_0(A,B)|(![D]: ((~r2_hidden(D,C)|(r2_hidden(D,A)&r2_hidden(D,B)))&(r2_hidden(D,C)|(~r2_hidden(D,A)|~r2_hidden(D,B))))))&(C=k3_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)|~r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)&r2_hidden(D,B)))))))),
% 269.83/46.30 inference(NNF_transformation,[status(thm)],[f31])).
% 269.83/46.30 fof(f66162,plain,(
% 269.83/46.30 (![A,B,C]: (~C=k3_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)&r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)|~r2_hidden(D,B)))))))&(![A,B,C]: (C=k3_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)|~r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)&r2_hidden(D,B)))))))),
% 269.83/46.30 inference(miniscoping,[status(thm)],[f66161])).
% 269.83/46.30 fof(f66163,plain,(
% 269.83/46.30 (![A,B,C]: (~C=k3_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)&r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)|~r2_hidden(D,B)))))))&(![A,B,C]: (C=k3_xboole_0(A,B)|((~r2_hidden(sK24_skl(C,B,A),C)|(~r2_hidden(sK24_skl(C,B,A),A)|~r2_hidden(sK24_skl(C,B,A),B)))&(r2_hidden(sK24_skl(C,B,A),C)|(r2_hidden(sK24_skl(C,B,A),A)&r2_hidden(sK24_skl(C,B,A),B))))))),
% 269.83/46.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(D,sK24_skl(C,B,A))],[f66162])).
% 269.83/46.30 fof(f66164,plain,(
% 269.83/46.30 ![X0,X1,X2,X3]: (~X0=k3_xboole_0(X1,X2)|~r2_hidden(X3,X0)|r2_hidden(X3,X1))),
% 269.83/46.30 inference(cnf_transformation,[status(thm)],[f66163])).
% 269.83/46.30 fof(f161583,plain,(
% 269.83/46.30 ![A]: (~l1_orders_2(A)|(~v1_lattice3(A)|~v3_struct_0(A)))),
% 269.83/46.30 inference(pre_NNF_transformation,[status(thm)],[f28604])).
% 269.83/46.30 fof(f161584,plain,(
% 269.83/46.30 ![X0]: (~l1_orders_2(X0)|~v1_lattice3(X0)|~v3_struct_0(X0))),
% 269.83/46.30 inference(cnf_transformation,[status(thm)],[f161583])).
% 269.83/46.30 fof(f216176,plain,(
% 269.83/46.30 ![A]: ((((v3_struct_0(A)|~v4_orders_2(A))|~v1_yellow_0(A))|~l1_orders_2(A))|(![B]: (((v1_xboole_0(B)|~v12_waybel_0(B,A))|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|r2_hidden(k3_yellow_0(A),B))))),
% 269.83/46.30 inference(pre_NNF_transformation,[status(thm)],[f42238])).
% 269.83/46.30 fof(f216177,plain,(
% 269.83/46.30 ![X0,X1]: (v3_struct_0(X0)|~v4_orders_2(X0)|~v1_yellow_0(X0)|~l1_orders_2(X0)|v1_xboole_0(X1)|~v12_waybel_0(X1,X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|r2_hidden(k3_yellow_0(X0),X1))),
% 269.83/46.30 inference(cnf_transformation,[status(thm)],[f216176])).
% 269.83/46.30 fof(f310278,plain,(
% 269.83/46.30 (?[A]: (((((((~v3_struct_0(A)&v2_orders_2(A))&v3_orders_2(A))&v4_orders_2(A))&v1_yellow_0(A))&v1_lattice3(A))&l1_orders_2(A))&(?[B]: (((((((~v3_struct_0(B)&v2_orders_2(B))&v3_orders_2(B))&v4_orders_2(B))&v1_yellow_0(B))&v1_lattice3(B))&l1_orders_2(B))&((((~v1_xboole_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))&v1_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B))&v12_waybel_0(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),B))&m1_subset_1(k3_xboole_0(u1_struct_0(A),u1_struct_0(B)),k1_zfmisc_1(u1_struct_0(B))))&~r2_hidden(k3_yellow_0(B),u1_struct_0(A)))))))),
% 269.83/46.30 inference(pre_NNF_transformation,[status(thm)],[f66057])).
% 269.83/46.30 fof(f310279,plain,(
% 269.83/46.30 (((((((~v3_struct_0(sK22359_skl)&v2_orders_2(sK22359_skl))&v3_orders_2(sK22359_skl))&v4_orders_2(sK22359_skl))&v1_yellow_0(sK22359_skl))&v1_lattice3(sK22359_skl))&l1_orders_2(sK22359_skl))&(((((((~v3_struct_0(sK22360_skl)&v2_orders_2(sK22360_skl))&v3_orders_2(sK22360_skl))&v4_orders_2(sK22360_skl))&v1_yellow_0(sK22360_skl))&v1_lattice3(sK22360_skl))&l1_orders_2(sK22360_skl))&((((~v1_xboole_0(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)))&v1_waybel_0(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)),sK22360_skl))&v12_waybel_0(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)),sK22360_skl))&m1_subset_1(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)),k1_zfmisc_1(u1_struct_0(sK22360_skl))))&~r2_hidden(k3_yellow_0(sK22360_skl),u1_struct_0(sK22359_skl)))))),
% 269.83/46.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK22359_skl,sK22360_skl]),skolemize(A,sK22359_skl),skolemize(B,sK22360_skl)],[f310278])).
% 269.83/46.30 fof(f310290,plain,(
% 269.83/46.30 v4_orders_2(sK22360_skl)),
% 269.83/46.30 inference(cnf_transformation,[status(thm)],[f310279])).
% 269.83/46.30 fof(f310291,plain,(
% 269.83/46.30 v1_yellow_0(sK22360_skl)),
% 269.83/46.30 inference(cnf_transformation,[status(thm)],[f310279])).
% 269.83/46.30 fof(f310292,plain,(
% 269.83/46.30 v1_lattice3(sK22360_skl)),
% 269.83/46.30 inference(cnf_transformation,[status(thm)],[f310279])).
% 269.83/46.30 fof(f310293,plain,(
% 269.83/46.30 l1_orders_2(sK22360_skl)),
% 269.83/46.30 inference(cnf_transformation,[status(thm)],[f310279])).
% 269.83/46.30 fof(f310294,plain,(
% 269.83/46.30 ~v1_xboole_0(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)))),
% 269.83/46.30 inference(cnf_transformation,[status(thm)],[f310279])).
% 269.83/46.30 fof(f310296,plain,(
% 269.83/46.30 v12_waybel_0(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)),sK22360_skl)),
% 269.83/46.30 inference(cnf_transformation,[status(thm)],[f310279])).
% 269.83/46.30 fof(f310297,plain,(
% 269.83/46.30 m1_subset_1(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)),k1_zfmisc_1(u1_struct_0(sK22360_skl)))),
% 269.83/46.30 inference(cnf_transformation,[status(thm)],[f310279])).
% 269.83/46.30 fof(f310298,plain,(
% 269.83/46.30 ~r2_hidden(k3_yellow_0(sK22360_skl),u1_struct_0(sK22359_skl))),
% 269.83/46.30 inference(cnf_transformation,[status(thm)],[f310279])).
% 269.83/46.30 fof(f364303,plain,(
% 269.83/46.30 ![X0,X1,X2]: (~r2_hidden(X0,k3_xboole_0(X1,X2))|r2_hidden(X0,X1))),
% 269.83/46.30 inference(destructive_equality_resolution,[status(thm)],[f66164])).
% 269.83/46.30 fof(f385144,definition,(
% 269.83/46.30 sQ6315_spl <=> (v1_xboole_0(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl))))),
% 269.83/46.30 introduced(definition,[new_symbols(definition,[sQ6315_spl])],[split_symbol_definition])).
% 269.83/46.30 fof(f385145,plain,(
% 269.83/46.30 v1_xboole_0(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)))|~sQ6315_spl),
% 269.83/46.30 inference(component_clause,[status(thm)],[f385144])).
% 269.83/46.30 fof(f389057,plain,(
% 269.83/46.30 ~l1_orders_2(sK22360_skl)|~v3_struct_0(sK22360_skl)),
% 269.83/46.30 inference(resolution,[status(thm)],[f161584,f310292])).
% 269.83/46.30 fof(f389059,definition,(
% 269.83/46.30 sQ6438_spl <=> (l1_orders_2(sK22360_skl))),
% 269.83/46.30 introduced(definition,[new_symbols(definition,[sQ6438_spl])],[split_symbol_definition])).
% 269.83/46.30 fof(f389061,plain,(
% 269.83/46.30 ~l1_orders_2(sK22360_skl)|sQ6438_spl),
% 269.83/46.30 inference(component_clause,[status(thm)],[f389059])).
% 269.83/46.30 fof(f389062,definition,(
% 269.83/46.30 sQ6439_spl <=> (v3_struct_0(sK22360_skl))),
% 269.83/46.30 introduced(definition,[new_symbols(definition,[sQ6439_spl])],[split_symbol_definition])).
% 269.83/46.30 fof(f389065,plain,(
% 220.68/47.79 ~sQ6438_spl|~sQ6439_spl),
% 220.68/47.79 inference(split_clause,[status(thm)],[f389057,f389059,f389062])).
% 220.68/47.79 fof(f389075,plain,(
% 220.68/47.79 $false|sQ6438_spl),
% 220.68/47.79 inference(forward_subsumption_resolution,[status(thm)],[f389061,f310293])).
% 220.68/47.79 fof(f389076,plain,(
% 220.68/47.79 sQ6438_spl),
% 220.68/47.79 inference(contradiction_clause,[status(thm)],[f389075])).
% 220.68/47.79 fof(f389114,plain,(
% 220.68/47.79 $false|~sQ6315_spl),
% 220.68/47.79 inference(forward_subsumption_resolution,[status(thm)],[f385145,f310294])).
% 220.68/47.79 fof(f389115,plain,(
% 220.68/47.79 ~sQ6315_spl),
% 220.68/47.79 inference(contradiction_clause,[status(thm)],[f389114])).
% 220.68/47.79 fof(f389417,definition,(
% 220.68/47.79 sQ6453_spl <=> (v12_waybel_0(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)),sK22360_skl))),
% 220.68/47.79 introduced(definition,[new_symbols(definition,[sQ6453_spl])],[split_symbol_definition])).
% 220.68/47.79 fof(f389419,plain,(
% 220.68/47.79 ~v12_waybel_0(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)),sK22360_skl)|sQ6453_spl),
% 220.68/47.79 inference(component_clause,[status(thm)],[f389417])).
% 220.68/47.79 fof(f389431,plain,(
% 220.68/47.79 $false|sQ6453_spl),
% 220.68/47.79 inference(forward_subsumption_resolution,[status(thm)],[f389419,f310296])).
% 220.68/47.79 fof(f389432,plain,(
% 220.68/47.79 sQ6453_spl),
% 220.68/47.79 inference(contradiction_clause,[status(thm)],[f389431])).
% 220.68/47.79 fof(f389726,definition,(
% 220.68/47.79 sQ6469_spl <=> (v4_orders_2(sK22360_skl))),
% 220.68/47.79 introduced(definition,[new_symbols(definition,[sQ6469_spl])],[split_symbol_definition])).
% 220.68/47.79 fof(f389728,plain,(
% 220.68/47.79 ~v4_orders_2(sK22360_skl)|sQ6469_spl),
% 220.68/47.79 inference(component_clause,[status(thm)],[f389726])).
% 220.68/47.79 fof(f389748,plain,(
% 220.68/47.79 $false|sQ6469_spl),
% 220.68/47.79 inference(forward_subsumption_resolution,[status(thm)],[f389728,f310290])).
% 220.68/47.79 fof(f389749,plain,(
% 220.68/47.79 sQ6469_spl),
% 220.68/47.79 inference(contradiction_clause,[status(thm)],[f389748])).
% 220.68/47.79 fof(f390184,definition,(
% 220.68/47.79 sQ6479_spl <=> (v1_yellow_0(sK22360_skl))),
% 220.68/47.79 introduced(definition,[new_symbols(definition,[sQ6479_spl])],[split_symbol_definition])).
% 220.68/47.79 fof(f390186,plain,(
% 220.68/47.79 ~v1_yellow_0(sK22360_skl)|sQ6479_spl),
% 220.68/47.79 inference(component_clause,[status(thm)],[f390184])).
% 220.68/47.79 fof(f390199,plain,(
% 220.68/47.79 $false|sQ6479_spl),
% 220.68/47.79 inference(forward_subsumption_resolution,[status(thm)],[f390186,f310291])).
% 220.68/47.79 fof(f390200,plain,(
% 220.68/47.79 sQ6479_spl),
% 220.68/47.79 inference(contradiction_clause,[status(thm)],[f390199])).
% 220.68/47.79 fof(f390773,definition,(
% 220.68/47.79 sQ6503_spl <=> (r2_hidden(k3_yellow_0(sK22360_skl),k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl))))),
% 220.68/47.79 introduced(definition,[new_symbols(definition,[sQ6503_spl])],[split_symbol_definition])).
% 220.68/47.79 fof(f390774,plain,(
% 220.68/47.79 r2_hidden(k3_yellow_0(sK22360_skl),k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)))|~sQ6503_spl),
% 220.68/47.79 inference(component_clause,[status(thm)],[f390773])).
% 220.68/47.79 fof(f391894,plain,(
% 220.68/47.79 v3_struct_0(sK22360_skl)|~v4_orders_2(sK22360_skl)|~v1_yellow_0(sK22360_skl)|~l1_orders_2(sK22360_skl)|v1_xboole_0(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)))|~v12_waybel_0(k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)),sK22360_skl)|r2_hidden(k3_yellow_0(sK22360_skl),k3_xboole_0(u1_struct_0(sK22359_skl),u1_struct_0(sK22360_skl)))),
% 220.68/47.79 inference(resolution,[status(thm)],[f216177,f310297])).
% 220.68/47.79 fof(f391896,plain,(
% 220.68/47.79 sQ6439_spl|~sQ6469_spl|~sQ6479_spl|~sQ6438_spl|sQ6315_spl|~sQ6453_spl|sQ6503_spl),
% 220.68/47.79 inference(split_clause,[status(thm)],[f391894,f389062,f389726,f390184,f389059,f385144,f389417,f390773])).
% 220.68/47.79 fof(f392683,plain,(
% 220.68/47.79 r2_hidden(k3_yellow_0(sK22360_skl),u1_struct_0(sK22359_skl))|~sQ6503_spl),
% 220.68/47.79 inference(resolution,[status(thm)],[f390774,f364303])).
% 220.68/47.79 fof(f392705,plain,(
% 220.68/47.79 $false|~sQ6503_spl),
% 220.68/47.79 inference(forward_subsumption_resolution,[status(thm)],[f392683,f310298])).
% 220.68/47.79 fof(f392706,plain,(
% 220.68/47.79 ~sQ6503_spl),
% 220.68/47.79 inference(contradiction_clause,[status(thm)],[f392705])).
% 220.68/47.79 fof(f392707,plain,(
% 220.68/47.79 $false),
% 220.68/47.79 inference(sat_refutation,[status(thm)],[f389065,f389076,f389115,f389432,f389749,f390200,f391896,f392706])).
% 220.68/47.79 % SZS output end CNFRefutation for theBenchmark.p
% 99.09/48.63 % Elapsed time: 47.388977 seconds
% 99.09/48.63 % CPU time: 273.956335 seconds
% 99.09/48.63 % Total memory used: 21.201 GB
% 99.09/48.63 % Net memory used: 21.007 GB
%------------------------------------------------------------------------------