%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU411+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 : n026.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 34.94s 7.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU411+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.15/0.42 % Computer : n026.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Mon Sep 21 06:25:10 UTC 2026
% 0.15/0.43 % CPUTime :
% 2.56/2.85 % Drodi V4.1.1
% 34.94/7.03 % Refutation found
% 34.94/7.03 % SZS status Theorem for theBenchmark: Theorem is valid
% 34.94/7.03 % SZS output start CNFRefutation for theBenchmark
% 34.94/7.03 fof(f31,axiom,(
% 34.94/7.03 (! [A,B,C] :( C = k3_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)& r2_hidden(D,B) ) ) )) )),
% 34.94/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 34.94/7.03 fof(f16772,axiom,(
% 34.94/7.03 (! [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) ) )) )),
% 34.94/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 34.94/7.03 fof(f19046,conjecture,(
% 34.94/7.03 (! [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)) ) ) )) )),
% 34.94/7.03 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 34.94/7.03 fof(f19047,negated_conjecture,(
% 34.94/7.03 ~((! [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)) ) ) )) ))),
% 34.94/7.03 inference(negated_conjecture,[status(cth)],[f19046])).
% 34.94/7.03 fof(f19151,plain,(
% 34.94/7.03 ![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)))))))),
% 34.94/7.03 inference(NNF_transformation,[status(thm)],[f31])).
% 34.94/7.03 fof(f19152,plain,(
% 34.94/7.03 (![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)))))))),
% 34.94/7.03 inference(miniscoping,[status(thm)],[f19151])).
% 34.94/7.03 fof(f19153,plain,(
% 34.94/7.03 (![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))))))),
% 34.94/7.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(D,sK24_skl(C,B,A))],[f19152])).
% 34.94/7.03 fof(f19154,plain,(
% 34.94/7.03 ![X0,X1,X2,X3]: (~X0=k3_xboole_0(X1,X2)|~r2_hidden(X3,X0)|r2_hidden(X3,X1))),
% 34.94/7.03 inference(cnf_transformation,[status(thm)],[f19153])).
% 34.94/7.03 fof(f77335,plain,(
% 34.94/7.03 ![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))))),
% 34.94/7.03 inference(pre_NNF_transformation,[status(thm)],[f16772])).
% 34.94/7.03 fof(f77336,plain,(
% 34.94/7.03 ![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))),
% 34.94/7.03 inference(cnf_transformation,[status(thm)],[f77335])).
% 34.94/7.03 fof(f89112,plain,(
% 34.94/7.03 (?[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)))))))),
% 34.94/7.03 inference(pre_NNF_transformation,[status(thm)],[f19047])).
% 34.94/7.03 fof(f89113,plain,(
% 34.94/7.03 (((((((~v3_struct_0(sK6520_skl)&v2_orders_2(sK6520_skl))&v3_orders_2(sK6520_skl))&v4_orders_2(sK6520_skl))&v1_yellow_0(sK6520_skl))&v1_lattice3(sK6520_skl))&l1_orders_2(sK6520_skl))&(((((((~v3_struct_0(sK6521_skl)&v2_orders_2(sK6521_skl))&v3_orders_2(sK6521_skl))&v4_orders_2(sK6521_skl))&v1_yellow_0(sK6521_skl))&v1_lattice3(sK6521_skl))&l1_orders_2(sK6521_skl))&((((~v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))&v1_waybel_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),sK6521_skl))&v12_waybel_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),sK6521_skl))&m1_subset_1(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),k1_zfmisc_1(u1_struct_0(sK6521_skl))))&~r2_hidden(k3_yellow_0(sK6521_skl),u1_struct_0(sK6520_skl)))))),
% 34.94/7.03 inference(skolemize,[status(esa),new_symbols(skolem,[sK6520_skl,sK6521_skl]),skolemize(A,sK6520_skl),skolemize(B,sK6521_skl)],[f89112])).
% 34.94/7.03 fof(f89121,plain,(
% 34.94/7.03 ~v3_struct_0(sK6521_skl)),
% 34.94/7.03 inference(cnf_transformation,[status(thm)],[f89113])).
% 34.94/7.03 fof(f89124,plain,(
% 34.94/7.03 v4_orders_2(sK6521_skl)),
% 34.94/7.03 inference(cnf_transformation,[status(thm)],[f89113])).
% 34.94/7.03 fof(f89125,plain,(
% 34.94/7.03 v1_yellow_0(sK6521_skl)),
% 34.94/7.03 inference(cnf_transformation,[status(thm)],[f89113])).
% 34.94/7.03 fof(f89127,plain,(
% 34.94/7.03 l1_orders_2(sK6521_skl)),
% 34.94/7.03 inference(cnf_transformation,[status(thm)],[f89113])).
% 34.94/7.03 fof(f89128,plain,(
% 34.94/7.03 ~v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))),
% 34.94/7.03 inference(cnf_transformation,[status(thm)],[f89113])).
% 34.94/7.03 fof(f89130,plain,(
% 34.94/7.03 v12_waybel_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),sK6521_skl)),
% 34.94/7.03 inference(cnf_transformation,[status(thm)],[f89113])).
% 34.94/7.03 fof(f89131,plain,(
% 34.94/7.03 m1_subset_1(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),k1_zfmisc_1(u1_struct_0(sK6521_skl)))),
% 34.94/7.03 inference(cnf_transformation,[status(thm)],[f89113])).
% 34.94/7.03 fof(f89132,plain,(
% 34.94/7.03 ~r2_hidden(k3_yellow_0(sK6521_skl),u1_struct_0(sK6520_skl))),
% 34.94/7.03 inference(cnf_transformation,[status(thm)],[f89113])).
% 34.94/7.03 fof(f95709,plain,(
% 34.94/7.03 ![X0,X1,X2]: (~r2_hidden(X0,k3_xboole_0(X1,X2))|r2_hidden(X0,X1))),
% 34.94/7.03 inference(destructive_equality_resolution,[status(thm)],[f19154])).
% 34.94/7.03 fof(f101709,plain,(
% 34.94/7.03 v3_struct_0(sK6521_skl)|~v4_orders_2(sK6521_skl)|~v1_yellow_0(sK6521_skl)|~l1_orders_2(sK6521_skl)|v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))|~v12_waybel_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),sK6521_skl)|r2_hidden(k3_yellow_0(sK6521_skl),k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))),
% 34.94/7.03 inference(resolution,[status(thm)],[f89131,f77336])).
% 34.94/7.03 fof(f101715,plain,(
% 34.94/7.03 ~v4_orders_2(sK6521_skl)|~v1_yellow_0(sK6521_skl)|~l1_orders_2(sK6521_skl)|v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))|~v12_waybel_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),sK6521_skl)|r2_hidden(k3_yellow_0(sK6521_skl),k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))),
% 34.94/7.03 inference(forward_subsumption_resolution,[status(thm)],[f101709,f89121])).
% 34.94/7.03 fof(f102045,plain,(
% 34.94/7.03 ~v1_yellow_0(sK6521_skl)|~l1_orders_2(sK6521_skl)|v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))|~v12_waybel_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)),sK6521_skl)|r2_hidden(k3_yellow_0(sK6521_skl),k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))),
% 34.94/7.03 inference(forward_subsumption_resolution,[status(thm)],[f101715,f89124])).
% 34.94/7.03 fof(f102046,plain,(
% 34.94/7.03 ~v1_yellow_0(sK6521_skl)|~l1_orders_2(sK6521_skl)|v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))|r2_hidden(k3_yellow_0(sK6521_skl),k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))),
% 36.78/7.32 inference(resolution,[status(thm)],[f102045,f89130])).
% 36.78/7.32 fof(f102049,plain,(
% 36.78/7.32 ~l1_orders_2(sK6521_skl)|v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))|r2_hidden(k3_yellow_0(sK6521_skl),k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))),
% 36.78/7.32 inference(forward_subsumption_resolution,[status(thm)],[f102046,f89125])).
% 36.78/7.32 fof(f107741,plain,(
% 36.78/7.32 v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))|r2_hidden(k3_yellow_0(sK6521_skl),k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))),
% 36.78/7.32 inference(forward_subsumption_resolution,[status(thm)],[f102049,f89127])).
% 36.78/7.32 fof(f107745,plain,(
% 36.78/7.32 v1_xboole_0(k3_xboole_0(u1_struct_0(sK6520_skl),u1_struct_0(sK6521_skl)))|r2_hidden(k3_yellow_0(sK6521_skl),u1_struct_0(sK6520_skl))),
% 36.78/7.32 inference(resolution,[status(thm)],[f107741,f95709])).
% 36.78/7.32 fof(f107778,plain,(
% 36.78/7.32 r2_hidden(k3_yellow_0(sK6521_skl),u1_struct_0(sK6520_skl))),
% 36.78/7.32 inference(forward_subsumption_resolution,[status(thm)],[f107745,f89128])).
% 36.78/7.32 fof(f109574,plain,(
% 36.78/7.32 $false),
% 36.78/7.32 inference(forward_subsumption_resolution,[status(thm)],[f107778,f89132])).
% 36.78/7.32 % SZS output end CNFRefutation for theBenchmark.p
% 3.58/7.65 % Elapsed time: 7.124423 seconds
% 3.58/7.65 % CPU time: 36.095523 seconds
% 3.58/7.65 % Total memory used: 5.354 GB
% 3.58/7.65 % Net memory used: 5.308 GB
%------------------------------------------------------------------------------