%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU411+1 : 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 4.78s 1.22s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU411+1 : 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.17/0.45 % Computer : n015.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 06:25:21 UTC 2026
% 0.17/0.46 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 4.78/1.22 % Refutation found
% 4.78/1.22 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.78/1.22 % SZS output start CNFRefutation for theBenchmark
% 4.78/1.22 fof(f1,conjecture,(
% 4.78/1.22 (! [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)) ) ) )) )),
% 4.78/1.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.78/1.22 fof(f2,negated_conjecture,(
% 4.78/1.22 ~((! [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)) ) ) )) ))),
% 4.78/1.22 inference(negated_conjecture,[status(cth)],[f1])).
% 4.78/1.22 fof(f4,axiom,(
% 4.78/1.22 (! [A,B] : k3_xboole_0(A,B) = k3_xboole_0(B,A) )),
% 4.78/1.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.78/1.22 fof(f5,axiom,(
% 4.78/1.22 (! [A] :( l1_orders_2(A)=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> ( v12_waybel_0(B,A)<=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> (! [D] :( m1_subset_1(D,u1_struct_0(A))=> ( ( r2_hidden(C,B)& r1_orders_2(A,D,C) )=> r2_hidden(D,B) ) ) )) )) ) )) )),
% 4.78/1.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.78/1.22 fof(f6,axiom,(
% 4.78/1.22 (! [A] :( A = k1_xboole_0<=> (! [B] : ~ r2_hidden(B,A) )) )),
% 4.78/1.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.78/1.22 fof(f7,axiom,(
% 4.78/1.22 (! [A,B,C] :( C = k3_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)& r2_hidden(D,B) ) ) )) )),
% 4.78/1.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.78/1.22 fof(f11,axiom,(
% 4.78/1.22 (! [A] :( l1_orders_2(A)=> m1_subset_1(k3_yellow_0(A),u1_struct_0(A)) ) )),
% 4.78/1.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.78/1.22 fof(f20,axiom,(
% 4.78/1.22 v1_xboole_0(k1_xboole_0) ),
% 4.78/1.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.78/1.22 fof(f30,axiom,(
% 4.78/1.22 (! [A] :( ( ~ v3_struct_0(A)& l1_orders_2(A) )=> (! [B] :( ( ~ v3_struct_0(B)& l1_orders_2(B) )=> (! [C] :( r2_hidden(C,k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))=> m1_subset_1(C,u1_struct_0(B)) ) )) )) )),
% 4.78/1.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.78/1.22 fof(f35,axiom,(
% 4.78/1.22 (! [A] :( ( ~ v3_struct_0(A)& v4_orders_2(A)& v1_yellow_0(A)& l1_orders_2(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> r1_orders_2(A,k3_yellow_0(A),B) ) )) )),
% 4.78/1.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.78/1.22 fof(f36,axiom,(
% 4.78/1.22 (! [A,B,C] :( ( r2_hidden(A,B)& m1_subset_1(B,k1_zfmisc_1(C)) )=> m1_subset_1(A,C) ) )),
% 4.78/1.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.78/1.22 fof(f41,plain,(
% 4.78/1.22 (?[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)))))))),
% 4.78/1.22 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 4.78/1.22 fof(f42,plain,(
% 4.78/1.22 (((((((~v3_struct_0(sK0_skl)&v2_orders_2(sK0_skl))&v3_orders_2(sK0_skl))&v4_orders_2(sK0_skl))&v1_yellow_0(sK0_skl))&v1_lattice3(sK0_skl))&l1_orders_2(sK0_skl))&(((((((~v3_struct_0(sK1_skl)&v2_orders_2(sK1_skl))&v3_orders_2(sK1_skl))&v4_orders_2(sK1_skl))&v1_yellow_0(sK1_skl))&v1_lattice3(sK1_skl))&l1_orders_2(sK1_skl))&((((~v1_xboole_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))&v1_waybel_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),sK1_skl))&v12_waybel_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),sK1_skl))&m1_subset_1(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl))))&~r2_hidden(k3_yellow_0(sK1_skl),u1_struct_0(sK0_skl)))))),
% 4.78/1.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f41])).
% 4.78/1.22 fof(f43,plain,(
% 4.78/1.22 ~v3_struct_0(sK0_skl)),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f42])).
% 4.78/1.22 fof(f49,plain,(
% 4.78/1.22 l1_orders_2(sK0_skl)),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f42])).
% 4.78/1.22 fof(f50,plain,(
% 4.78/1.22 ~v3_struct_0(sK1_skl)),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f42])).
% 4.78/1.22 fof(f53,plain,(
% 4.78/1.22 v4_orders_2(sK1_skl)),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f42])).
% 4.78/1.22 fof(f54,plain,(
% 4.78/1.22 v1_yellow_0(sK1_skl)),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f42])).
% 4.78/1.22 fof(f56,plain,(
% 4.78/1.22 l1_orders_2(sK1_skl)),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f42])).
% 4.78/1.22 fof(f57,plain,(
% 4.78/1.22 ~v1_xboole_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f42])).
% 4.78/1.22 fof(f59,plain,(
% 4.78/1.22 v12_waybel_0(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),sK1_skl)),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f42])).
% 4.78/1.22 fof(f60,plain,(
% 4.78/1.22 m1_subset_1(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl)))),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f42])).
% 4.78/1.22 fof(f61,plain,(
% 4.78/1.22 ~r2_hidden(k3_yellow_0(sK1_skl),u1_struct_0(sK0_skl))),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f42])).
% 4.78/1.22 fof(f64,plain,(
% 4.78/1.22 ![X0,X1]: (k3_xboole_0(X0,X1)=k3_xboole_0(X1,X0))),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f4])).
% 4.78/1.22 fof(f65,plain,(
% 4.78/1.22 ![A]: (~l1_orders_2(A)|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|(v12_waybel_0(B,A)<=>(![C]: (~m1_subset_1(C,u1_struct_0(A))|(![D]: (~m1_subset_1(D,u1_struct_0(A))|((~r2_hidden(C,B)|~r1_orders_2(A,D,C))|r2_hidden(D,B))))))))))),
% 4.78/1.22 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 4.78/1.22 fof(f66,plain,(
% 4.78/1.22 ![A]: (~l1_orders_2(A)|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|((~v12_waybel_0(B,A)|(![C]: (~m1_subset_1(C,u1_struct_0(A))|(![D]: (~m1_subset_1(D,u1_struct_0(A))|((~r2_hidden(C,B)|~r1_orders_2(A,D,C))|r2_hidden(D,B)))))))&(v12_waybel_0(B,A)|(?[C]: (m1_subset_1(C,u1_struct_0(A))&(?[D]: (m1_subset_1(D,u1_struct_0(A))&((r2_hidden(C,B)&r1_orders_2(A,D,C))&~r2_hidden(D,B)))))))))))),
% 4.78/1.22 inference(NNF_transformation,[status(thm)],[f65])).
% 4.78/1.22 fof(f67,plain,(
% 4.78/1.22 ![A]: (~l1_orders_2(A)|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|((~v12_waybel_0(B,A)|(![C]: (~m1_subset_1(C,u1_struct_0(A))|(![D]: (~m1_subset_1(D,u1_struct_0(A))|((~r2_hidden(C,B)|~r1_orders_2(A,D,C))|r2_hidden(D,B)))))))&(v12_waybel_0(B,A)|(m1_subset_1(sK2_skl(B,A),u1_struct_0(A))&(m1_subset_1(sK3_skl(B,A),u1_struct_0(A))&((r2_hidden(sK2_skl(B,A),B)&r1_orders_2(A,sK3_skl(B,A),sK2_skl(B,A)))&~r2_hidden(sK3_skl(B,A),B)))))))))),
% 4.78/1.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(C,sK2_skl(B,A)),skolemize(D,sK3_skl(B,A))],[f66])).
% 4.78/1.22 fof(f68,plain,(
% 4.78/1.22 ![X0,X1,X2,X3]: (~l1_orders_2(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v12_waybel_0(X1,X0)|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X3,u1_struct_0(X0))|~r2_hidden(X2,X1)|~r1_orders_2(X0,X3,X2)|r2_hidden(X3,X1))),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f67])).
% 4.78/1.22 fof(f74,plain,(
% 4.78/1.22 ![A]: ((~A=k1_xboole_0|(![B]: ~r2_hidden(B,A)))&(A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 4.78/1.22 inference(NNF_transformation,[status(thm)],[f6])).
% 4.78/1.22 fof(f75,plain,(
% 4.78/1.22 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 4.78/1.22 inference(miniscoping,[status(thm)],[f74])).
% 4.78/1.22 fof(f76,plain,(
% 4.78/1.22 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|r2_hidden(sK4_skl(A),A)))),
% 4.78/1.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(B,sK4_skl(A))],[f75])).
% 4.78/1.22 fof(f77,plain,(
% 4.78/1.22 ![X0,X1]: (~X0=k1_xboole_0|~r2_hidden(X1,X0))),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f76])).
% 4.78/1.22 fof(f79,plain,(
% 4.78/1.22 ![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)))))))),
% 4.78/1.22 inference(NNF_transformation,[status(thm)],[f7])).
% 4.78/1.22 fof(f80,plain,(
% 4.78/1.22 (![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)))))))),
% 4.78/1.22 inference(miniscoping,[status(thm)],[f79])).
% 4.78/1.22 fof(f81,plain,(
% 4.78/1.22 (![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(sK5_skl(C,B,A),C)|(~r2_hidden(sK5_skl(C,B,A),A)|~r2_hidden(sK5_skl(C,B,A),B)))&(r2_hidden(sK5_skl(C,B,A),C)|(r2_hidden(sK5_skl(C,B,A),A)&r2_hidden(sK5_skl(C,B,A),B))))))),
% 4.78/1.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(D,sK5_skl(C,B,A))],[f80])).
% 4.78/1.22 fof(f82,plain,(
% 4.78/1.22 ![X0,X1,X2,X3]: (~X0=k3_xboole_0(X1,X2)|~r2_hidden(X3,X0)|r2_hidden(X3,X1))),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f81])).
% 4.78/1.22 fof(f86,plain,(
% 4.78/1.22 ![X0,X1,X2]: (X0=k3_xboole_0(X1,X2)|r2_hidden(sK5_skl(X0,X2,X1),X0)|r2_hidden(sK5_skl(X0,X2,X1),X1))),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f81])).
% 4.78/1.22 fof(f88,plain,(
% 4.78/1.22 ![A]: (~l1_orders_2(A)|m1_subset_1(k3_yellow_0(A),u1_struct_0(A)))),
% 4.78/1.22 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 4.78/1.22 fof(f89,plain,(
% 4.78/1.22 ![X0]: (~l1_orders_2(X0)|m1_subset_1(k3_yellow_0(X0),u1_struct_0(X0)))),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f88])).
% 4.78/1.22 fof(f100,plain,(
% 4.78/1.22 v1_xboole_0(k1_xboole_0)),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f20])).
% 4.78/1.22 fof(f129,plain,(
% 4.78/1.22 ![A]: ((v3_struct_0(A)|~l1_orders_2(A))|(![B]: ((v3_struct_0(B)|~l1_orders_2(B))|(![C]: (~r2_hidden(C,k3_xboole_0(u1_struct_0(A),u1_struct_0(B)))|m1_subset_1(C,u1_struct_0(B)))))))),
% 4.78/1.22 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 4.78/1.22 fof(f130,plain,(
% 4.78/1.22 ![X0,X1,X2]: (v3_struct_0(X0)|~l1_orders_2(X0)|v3_struct_0(X1)|~l1_orders_2(X1)|~r2_hidden(X2,k3_xboole_0(u1_struct_0(X0),u1_struct_0(X1)))|m1_subset_1(X2,u1_struct_0(X1)))),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f129])).
% 4.78/1.22 fof(f140,plain,(
% 4.78/1.22 ![A]: ((((v3_struct_0(A)|~v4_orders_2(A))|~v1_yellow_0(A))|~l1_orders_2(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|r1_orders_2(A,k3_yellow_0(A),B))))),
% 4.78/1.22 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 4.78/1.22 fof(f141,plain,(
% 4.78/1.22 ![X0,X1]: (v3_struct_0(X0)|~v4_orders_2(X0)|~v1_yellow_0(X0)|~l1_orders_2(X0)|~m1_subset_1(X1,u1_struct_0(X0))|r1_orders_2(X0,k3_yellow_0(X0),X1))),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f140])).
% 4.78/1.22 fof(f142,plain,(
% 4.78/1.22 ![A,B,C]: ((~r2_hidden(A,B)|~m1_subset_1(B,k1_zfmisc_1(C)))|m1_subset_1(A,C))),
% 4.78/1.22 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 4.78/1.22 fof(f143,plain,(
% 4.78/1.22 ![A,C]: ((![B]: (~r2_hidden(A,B)|~m1_subset_1(B,k1_zfmisc_1(C))))|m1_subset_1(A,C))),
% 4.78/1.22 inference(miniscoping,[status(thm)],[f142])).
% 4.78/1.22 fof(f144,plain,(
% 4.78/1.22 ![X0,X1,X2]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(X2))|m1_subset_1(X0,X2))),
% 4.78/1.22 inference(cnf_transformation,[status(thm)],[f143])).
% 4.78/1.22 fof(f156,plain,(
% 4.78/1.22 ![X0]: (~r2_hidden(X0,k1_xboole_0))),
% 4.78/1.22 inference(destructive_equality_resolution,[status(thm)],[f77])).
% 4.78/1.22 fof(f157,plain,(
% 4.78/1.22 ![X0,X1,X2]: (~r2_hidden(X0,k3_xboole_0(X1,X2))|r2_hidden(X0,X1))),
% 4.78/1.22 inference(destructive_equality_resolution,[status(thm)],[f82])).
% 4.78/1.22 fof(f177,plain,(
% 4.78/1.22 ![X0,X1,X2]: (~l1_orders_2(X0)|~l1_orders_2(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v12_waybel_0(X1,X0)|~m1_subset_1(X2,u1_struct_0(X0))|~r2_hidden(X2,X1)|~r1_orders_2(X0,k3_yellow_0(X0),X2)|r2_hidden(k3_yellow_0(X0),X1))),
% 4.78/1.22 inference(resolution,[status(thm)],[f89,f68])).
% 4.78/1.22 fof(f178,plain,(
% 4.78/1.22 ![X0,X1,X2]: (~l1_orders_2(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v12_waybel_0(X1,X0)|~m1_subset_1(X2,u1_struct_0(X0))|~r2_hidden(X2,X1)|~r1_orders_2(X0,k3_yellow_0(X0),X2)|r2_hidden(k3_yellow_0(X0),X1))),
% 4.78/1.22 inference(duplicate_literals_removal,[status(thm)],[f177])).
% 4.78/1.22 fof(f191,plain,(
% 4.78/1.22 ![X0,X1]: (v3_struct_0(X0)|~l1_orders_2(X0)|v3_struct_0(sK1_skl)|~r2_hidden(X1,k3_xboole_0(u1_struct_0(X0),u1_struct_0(sK1_skl)))|m1_subset_1(X1,u1_struct_0(sK1_skl)))),
% 4.78/1.22 inference(resolution,[status(thm)],[f130,f56])).
% 4.78/1.22 fof(f200,definition,(
% 4.78/1.22 ![X0,X1]: (sQ4_spl <=> (v3_struct_0(X0)|~l1_orders_2(X0)|~r2_hidden(X1,k3_xboole_0(u1_struct_0(X0),u1_struct_0(sK1_skl)))|m1_subset_1(X1,u1_struct_0(sK1_skl))))),
% 4.78/1.22 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 4.78/1.22 fof(f201,plain,(
% 4.78/1.22 ![X0,X1]: (v3_struct_0(X0)|~l1_orders_2(X0)|~r2_hidden(X1,k3_xboole_0(u1_struct_0(X0),u1_struct_0(sK1_skl)))|m1_subset_1(X1,u1_struct_0(sK1_skl))|~sQ4_spl)),
% 4.78/1.22 inference(component_clause,[status(thm)],[f200])).
% 4.78/1.22 fof(f203,definition,(
% 4.78/1.22 sQ5_spl <=> (v3_struct_0(sK1_skl))),
% 4.78/1.22 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 4.78/1.22 fof(f204,plain,(
% 4.78/1.22 v3_struct_0(sK1_skl)|~sQ5_spl),
% 4.78/1.22 inference(component_clause,[status(thm)],[f203])).
% 4.78/1.22 fof(f206,plain,(
% 4.78/1.22 sQ4_spl|sQ5_spl),
% 4.78/1.22 inference(split_clause,[status(thm)],[f191,f200,f203])).
% 4.78/1.22 fof(f210,definition,(
% 4.78/1.22 sQ7_spl <=> (v3_struct_0(sK0_skl))),
% 4.78/1.22 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 4.78/1.22 fof(f211,plain,(
% 4.78/1.22 v3_struct_0(sK0_skl)|~sQ7_spl),
% 4.78/1.22 inference(component_clause,[status(thm)],[f210])).
% 4.78/1.22 fof(f224,definition,(
% 4.78/1.22 sQ8_spl <=> (l1_orders_2(sK1_skl))),
% 4.78/1.22 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 4.78/1.22 fof(f226,plain,(
% 4.78/1.22 ~l1_orders_2(sK1_skl)|sQ8_spl),
% 4.78/1.22 inference(component_clause,[status(thm)],[f224])).
% 4.78/1.22 fof(f249,plain,(
% 4.78/1.22 $false|~sQ5_spl),
% 4.78/1.22 inference(forward_subsumption_resolution,[status(thm)],[f204,f50])).
% 4.78/1.22 fof(f250,plain,(
% 4.78/1.22 ~sQ5_spl),
% 4.78/1.22 inference(contradiction_clause,[status(thm)],[f249])).
% 4.78/1.22 fof(f251,plain,(
% 4.78/1.22 $false|~sQ7_spl),
% 4.78/1.22 inference(forward_subsumption_resolution,[status(thm)],[f211,f43])).
% 4.78/1.22 fof(f252,plain,(
% 4.78/1.22 ~sQ7_spl),
% 4.78/1.22 inference(contradiction_clause,[status(thm)],[f251])).
% 4.78/1.22 fof(f321,definition,(
% 4.78/1.22 sQ20_spl <=> (k3_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))=k1_xboole_0)),
% 4.78/1.22 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 4.78/1.22 fof(f322,plain,(
% 4.78/1.22 k3_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))=k1_xboole_0|~sQ20_spl),
% 4.78/1.22 inference(component_clause,[status(thm)],[f321])).
% 4.78/1.22 fof(f323,plain,(
% 4.78/1.22 ~k3_xboole_0(u1_struct_0(sK1_skl),u1_struct_0(sK0_skl))=k1_xboole_0|sQ20_spl),
% 4.78/1.22 inference(component_clause,[status(thm)],[f321])).
% 4.78/1.22 fof(f333,plain,(
% 4.78/1.22 ![X0]: (v3_struct_0(sK0_skl)|~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))|m1_subset_1(X0,u1_struct_0(sK1_skl))|~sQ4_spl)),
% 4.78/1.22 inference(resolution,[status(thm)],[f201,f49])).
% 4.78/1.22 fof(f342,definition,(
% 4.78/1.22 ![X0]: (sQ24_spl <=> (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))|m1_subset_1(X0,u1_struct_0(sK1_skl))))),
% 4.78/1.22 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 4.78/1.22 fof(f343,plain,(
% 4.78/1.22 ![X0]: (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))|m1_subset_1(X0,u1_struct_0(sK1_skl))|~sQ24_spl)),
% 4.78/1.22 inference(component_clause,[status(thm)],[f342])).
% 4.78/1.22 fof(f345,plain,(
% 4.78/1.22 sQ7_spl|sQ24_spl|~sQ4_spl),
% 4.78/1.22 inference(split_clause,[status(thm)],[f333,f210,f342,f200])).
% 4.78/1.22 fof(f351,plain,(
% 4.78/1.22 ![X0,X1,X2]: (~l1_orders_2(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v12_waybel_0(X1,X0)|~r2_hidden(X2,X1)|~r1_orders_2(X0,k3_yellow_0(X0),X2)|r2_hidden(k3_yellow_0(X0),X1))),
% 4.78/1.22 inference(forward_subsumption_resolution,[status(thm)],[f178,f144])).
% 4.78/1.22 fof(f352,plain,(
% 4.78/1.22 ![X0]: (~l1_orders_2(sK1_skl)|~m1_subset_1(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl)))|~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))|~r1_orders_2(sK1_skl,k3_yellow_0(sK1_skl),X0)|r2_hidden(k3_yellow_0(sK1_skl),k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))))),
% 4.78/1.22 inference(resolution,[status(thm)],[f351,f59])).
% 4.78/1.22 fof(f353,definition,(
% 4.78/1.22 sQ25_spl <=> (m1_subset_1(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl))))),
% 4.78/1.22 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 4.78/1.22 fof(f355,plain,(
% 4.78/1.22 ~m1_subset_1(k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)),k1_zfmisc_1(u1_struct_0(sK1_skl)))|sQ25_spl),
% 4.78/1.22 inference(component_clause,[status(thm)],[f353])).
% 4.78/1.22 fof(f356,definition,(
% 4.78/1.22 ![X0]: (sQ26_spl <=> (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))|~r1_orders_2(sK1_skl,k3_yellow_0(sK1_skl),X0)))),
% 4.78/1.22 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 4.78/1.22 fof(f357,plain,(
% 4.78/1.22 ![X0]: (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))|~r1_orders_2(sK1_skl,k3_yellow_0(sK1_skl),X0)|~sQ26_spl)),
% 4.78/1.22 inference(component_clause,[status(thm)],[f356])).
% 4.78/1.22 fof(f359,definition,(
% 4.78/1.22 sQ27_spl <=> (r2_hidden(k3_yellow_0(sK1_skl),k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))))),
% 4.78/1.22 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 4.78/1.22 fof(f360,plain,(
% 4.78/1.22 r2_hidden(k3_yellow_0(sK1_skl),k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))|~sQ27_spl),
% 4.78/1.22 inference(component_clause,[status(thm)],[f359])).
% 4.78/1.22 fof(f362,plain,(
% 4.78/1.22 ~sQ8_spl|~sQ25_spl|sQ26_spl|sQ27_spl),
% 4.78/1.22 inference(split_clause,[status(thm)],[f352,f224,f353,f356,f359])).
% 4.78/1.22 fof(f363,plain,(
% 4.78/1.22 $false|sQ8_spl),
% 4.78/1.22 inference(forward_subsumption_resolution,[status(thm)],[f226,f56])).
% 4.78/1.22 fof(f364,plain,(
% 4.78/1.22 sQ8_spl),
% 4.78/1.22 inference(contradiction_clause,[status(thm)],[f363])).
% 4.78/1.22 fof(f374,plain,(
% 4.78/1.22 k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))=k1_xboole_0|~sQ20_spl),
% 4.78/1.22 inference(paramodulation,[status(thm)],[f64,f322])).
% 4.78/1.22 fof(f383,plain,(
% 4.78/1.22 ~v1_xboole_0(k1_xboole_0)|~sQ20_spl),
% 4.78/1.22 inference(backward_demodulation,[status(thm)],[f374,f57])).
% 4.78/1.22 fof(f390,plain,(
% 4.78/1.22 ![X0]: (k1_xboole_0=k3_xboole_0(k1_xboole_0,X0))),
% 4.78/1.22 inference(resolution,[status(thm)],[f86,f156])).
% 4.78/1.22 fof(f414,plain,(
% 4.78/1.22 ![X0,X1]: (X0=k3_xboole_0(k1_xboole_0,X1)|r2_hidden(sK5_skl(X0,X1,k1_xboole_0),X0))),
% 4.78/1.22 inference(resolution,[status(thm)],[f86,f156])).
% 4.78/1.22 fof(f504,plain,(
% 4.78/1.22 ~k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))=k1_xboole_0|sQ20_spl),
% 4.78/1.22 inference(paramodulation,[status(thm)],[f64,f323])).
% 4.78/1.22 fof(f522,plain,(
% 4.78/1.22 $false|sQ25_spl),
% 4.78/1.22 inference(forward_subsumption_resolution,[status(thm)],[f355,f60])).
% 4.78/1.22 fof(f523,plain,(
% 4.78/1.22 sQ25_spl),
% 4.78/1.22 inference(contradiction_clause,[status(thm)],[f522])).
% 4.78/1.22 fof(f524,plain,(
% 4.78/1.22 $false|~sQ20_spl),
% 4.78/1.22 inference(forward_subsumption_resolution,[status(thm)],[f383,f100])).
% 4.78/1.22 fof(f525,plain,(
% 4.78/1.22 ~sQ20_spl),
% 4.78/1.22 inference(contradiction_clause,[status(thm)],[f524])).
% 4.78/1.22 fof(f856,definition,(
% 4.78/1.22 sQ55_spl <=> (k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))=k1_xboole_0)),
% 4.78/1.22 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 4.78/1.22 fof(f857,plain,(
% 4.78/1.22 k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))=k1_xboole_0|~sQ55_spl),
% 4.78/1.22 inference(component_clause,[status(thm)],[f856])).
% 4.78/1.22 fof(f863,plain,(
% 4.78/1.22 $false|sQ20_spl|~sQ55_spl),
% 4.78/1.22 inference(forward_subsumption_resolution,[status(thm)],[f857,f504])).
% 4.78/1.22 fof(f864,plain,(
% 4.78/1.22 sQ20_spl|~sQ55_spl),
% 4.78/1.22 inference(contradiction_clause,[status(thm)],[f863])).
% 4.78/1.22 fof(f2362,plain,(
% 4.78/1.22 ![X0,X1]: (X0=k1_xboole_0|r2_hidden(sK5_skl(X0,X1,k1_xboole_0),X0))),
% 4.78/1.22 inference(forward_demodulation,[status(thm)],[f390,f414])).
% 4.78/1.22 fof(f2552,plain,(
% 4.78/1.22 ![X0]: (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))|v3_struct_0(sK1_skl)|~v4_orders_2(sK1_skl)|~v1_yellow_0(sK1_skl)|~l1_orders_2(sK1_skl)|~m1_subset_1(X0,u1_struct_0(sK1_skl))|~sQ26_spl)),
% 4.78/1.22 inference(resolution,[status(thm)],[f357,f141])).
% 4.78/1.22 fof(f2553,definition,(
% 4.78/1.22 ![X0]: (sQ109_spl <=> (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))|~m1_subset_1(X0,u1_struct_0(sK1_skl))))),
% 4.78/1.22 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 4.78/1.23 fof(f2554,plain,(
% 4.78/1.23 ![X0]: (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))|~m1_subset_1(X0,u1_struct_0(sK1_skl))|~sQ109_spl)),
% 4.78/1.23 inference(component_clause,[status(thm)],[f2553])).
% 4.78/1.23 fof(f2556,definition,(
% 4.78/1.23 sQ110_spl <=> (v4_orders_2(sK1_skl))),
% 4.78/1.23 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 4.78/1.23 fof(f2558,plain,(
% 4.78/1.23 ~v4_orders_2(sK1_skl)|sQ110_spl),
% 4.78/1.23 inference(component_clause,[status(thm)],[f2556])).
% 4.78/1.23 fof(f2559,definition,(
% 4.78/1.23 sQ111_spl <=> (v1_yellow_0(sK1_skl))),
% 4.78/1.23 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 4.78/1.23 fof(f2561,plain,(
% 4.78/1.23 ~v1_yellow_0(sK1_skl)|sQ111_spl),
% 4.78/1.23 inference(component_clause,[status(thm)],[f2559])).
% 4.78/1.23 fof(f2562,plain,(
% 4.78/1.23 sQ109_spl|sQ5_spl|~sQ110_spl|~sQ111_spl|~sQ8_spl|~sQ26_spl),
% 4.78/1.23 inference(split_clause,[status(thm)],[f2552,f2553,f203,f2556,f2559,f224,f356])).
% 4.78/1.23 fof(f2568,plain,(
% 4.78/1.23 $false|sQ111_spl),
% 4.78/1.23 inference(forward_subsumption_resolution,[status(thm)],[f2561,f54])).
% 4.78/1.23 fof(f2569,plain,(
% 4.78/1.23 sQ111_spl),
% 4.78/1.23 inference(contradiction_clause,[status(thm)],[f2568])).
% 4.78/1.23 fof(f2570,plain,(
% 4.78/1.23 ![X0]: (~r2_hidden(X0,k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))|~sQ24_spl|~sQ109_spl)),
% 4.78/1.23 inference(forward_subsumption_resolution,[status(thm)],[f2554,f343])).
% 4.78/1.23 fof(f2586,plain,(
% 4.78/1.23 k3_xboole_0(u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))=k1_xboole_0|~sQ24_spl|~sQ109_spl),
% 4.78/1.23 inference(resolution,[status(thm)],[f2570,f2362])).
% 4.78/1.23 fof(f2601,plain,(
% 4.78/1.23 sQ55_spl|~sQ24_spl|~sQ109_spl),
% 4.78/1.23 inference(split_clause,[status(thm)],[f2586,f856,f342,f2553])).
% 4.78/1.23 fof(f2603,plain,(
% 4.78/1.23 $false|sQ110_spl),
% 4.78/1.23 inference(forward_subsumption_resolution,[status(thm)],[f2558,f53])).
% 4.78/1.23 fof(f2604,plain,(
% 4.78/1.23 sQ110_spl),
% 4.78/1.23 inference(contradiction_clause,[status(thm)],[f2603])).
% 4.78/1.23 fof(f2765,plain,(
% 4.78/1.23 r2_hidden(k3_yellow_0(sK1_skl),u1_struct_0(sK0_skl))|~sQ27_spl),
% 4.78/1.23 inference(resolution,[status(thm)],[f360,f157])).
% 4.78/1.23 fof(f2772,plain,(
% 4.78/1.23 $false|~sQ27_spl),
% 4.78/1.23 inference(forward_subsumption_resolution,[status(thm)],[f2765,f61])).
% 4.78/1.23 fof(f2773,plain,(
% 4.78/1.23 ~sQ27_spl),
% 4.78/1.23 inference(contradiction_clause,[status(thm)],[f2772])).
% 4.78/1.23 fof(f2774,plain,(
% 4.78/1.23 $false),
% 4.78/1.23 inference(sat_refutation,[status(thm)],[f206,f250,f252,f345,f362,f364,f523,f525,f864,f2562,f2569,f2601,f2604,f2773])).
% 4.78/1.23 % SZS output end CNFRefutation for theBenchmark.p
% 2.97/1.26 % Elapsed time: 0.784919 seconds
% 2.97/1.26 % CPU time: 5.643963 seconds
% 2.97/1.26 % Total memory used: 157.207 MB
% 2.97/1.26 % Net memory used: 153.655 MB
%------------------------------------------------------------------------------