%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CAT033+2 : 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 : n018.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 12:07:54 PM UTC 2026
% Result : Theorem 20.66s 3.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT033+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 14:02:59 UTC 2026
% 0.12/0.35 % CPUTime :
% 0.46/0.75 % Drodi V4.1.1
% 20.66/3.38 % Refutation found
% 20.66/3.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.66/3.38 % SZS output start CNFRefutation for theBenchmark
% 20.66/3.38 fof(f18,axiom,(
% 20.66/3.38 (! [A,B] : r1_tarski(A,A) )),
% 20.66/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.66/3.38 fof(f3063,axiom,(
% 20.66/3.38 (? [A] :( l1_cat_1(A)& v2_cat_1(A) ) )),
% 20.66/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.66/3.38 fof(f3064,axiom,(
% 20.66/3.38 (? [A] :( l1_cat_1(A)& v1_cat_1(A)& v2_cat_1(A) ) )),
% 20.66/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.66/3.38 fof(f3237,axiom,(
% 20.66/3.38 (! [A,B] :( v1_cat_1(k8_cat_1(A,B))& v2_cat_1(k8_cat_1(A,B))& l1_cat_1(k8_cat_1(A,B)) ) )),
% 20.66/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.66/3.38 fof(f3471,axiom,(
% 20.66/3.38 (? [A] :( l1_cat_1(A)& v2_cat_1(A)& v2_nattra_1(A) ) )),
% 20.66/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.66/3.38 fof(f3584,axiom,(
% 20.66/3.38 (! [A] :( ( v2_cat_1(A)& l1_cat_1(A) )=> ~ v1_xboole_0(k17_ens_1(A)) ) )),
% 20.66/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.66/3.38 fof(f3651,axiom,(
% 20.66/3.38 (! [A] :( ~ v1_xboole_0(A)=> (! [B] :( ( v2_cat_1(B)& l1_cat_1(B) )=> (! [C] :( m1_subset_1(C,u1_cat_1(B))=> ( r1_tarski(k17_ens_1(B),A)=> m2_cat_1(k20_ens_1(B,C),B,k12_ens_1(A)) ) ) )) )) )),
% 20.66/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.66/3.38 fof(f3800,axiom,(
% 20.66/3.38 (! [A] :( ( v2_cat_1(A)& l1_cat_1(A) )=> k1_yoneda_1(A) = k12_ens_1(k17_ens_1(A)) ) )),
% 20.66/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.66/3.38 fof(f3802,conjecture,(
% 20.66/3.38 (! [A] :( ( v2_cat_1(A)& l1_cat_1(A) )=> (! [B] :( m1_subset_1(B,u1_cat_1(A))=> m2_cat_1(k20_ens_1(A,B),A,k1_yoneda_1(A)) ) )) )),
% 20.66/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.66/3.38 fof(f3803,negated_conjecture,(
% 20.66/3.38 ~((! [A] :( ( v2_cat_1(A)& l1_cat_1(A) )=> (! [B] :( m1_subset_1(B,u1_cat_1(A))=> m2_cat_1(k20_ens_1(A,B),A,k1_yoneda_1(A)) ) )) ))),
% 20.66/3.38 inference(negated_conjecture,[status(cth)],[f3802])).
% 20.66/3.38 fof(f3879,plain,(
% 20.66/3.38 ![A]: r1_tarski(A,A)),
% 20.66/3.38 inference(miniscoping,[status(thm)],[f18])).
% 20.66/3.38 fof(f3880,plain,(
% 20.66/3.38 ![X0]: (r1_tarski(X0,X0))),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f3879])).
% 20.66/3.38 fof(f13039,plain,(
% 20.66/3.38 (l1_cat_1(sK981_skl)&v2_cat_1(sK981_skl))),
% 20.66/3.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK981_skl]),skolemize(A,sK981_skl)],[f3063])).
% 20.66/3.38 fof(f13040,plain,(
% 20.66/3.38 l1_cat_1(sK981_skl)),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f13039])).
% 20.66/3.38 fof(f13041,plain,(
% 20.66/3.38 v2_cat_1(sK981_skl)),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f13039])).
% 20.66/3.38 fof(f13042,plain,(
% 20.66/3.38 ((l1_cat_1(sK982_skl)&v1_cat_1(sK982_skl))&v2_cat_1(sK982_skl))),
% 20.66/3.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK982_skl]),skolemize(A,sK982_skl)],[f3064])).
% 20.66/3.38 fof(f13043,plain,(
% 20.66/3.38 l1_cat_1(sK982_skl)),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f13042])).
% 20.66/3.38 fof(f13045,plain,(
% 20.66/3.38 v2_cat_1(sK982_skl)),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f13042])).
% 20.66/3.38 fof(f13522,plain,(
% 20.66/3.38 ((![A,B]: v1_cat_1(k8_cat_1(A,B)))&(![A,B]: v2_cat_1(k8_cat_1(A,B))))&(![A,B]: l1_cat_1(k8_cat_1(A,B)))),
% 20.66/3.38 inference(miniscoping,[status(thm)],[f3237])).
% 20.66/3.38 fof(f13524,plain,(
% 20.66/3.38 ![X0,X1]: (v2_cat_1(k8_cat_1(X0,X1)))),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f13522])).
% 20.66/3.38 fof(f13525,plain,(
% 20.66/3.38 ![X0,X1]: (l1_cat_1(k8_cat_1(X0,X1)))),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f13522])).
% 20.66/3.38 fof(f14168,plain,(
% 20.66/3.38 ((l1_cat_1(sK1076_skl)&v2_cat_1(sK1076_skl))&v2_nattra_1(sK1076_skl))),
% 20.66/3.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK1076_skl]),skolemize(A,sK1076_skl)],[f3471])).
% 20.66/3.38 fof(f14169,plain,(
% 20.66/3.38 l1_cat_1(sK1076_skl)),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f14168])).
% 20.66/3.38 fof(f14170,plain,(
% 20.66/3.38 v2_cat_1(sK1076_skl)),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f14168])).
% 20.66/3.38 fof(f14567,plain,(
% 20.66/3.38 ![A]: ((~v2_cat_1(A)|~l1_cat_1(A))|~v1_xboole_0(k17_ens_1(A)))),
% 20.66/3.38 inference(pre_NNF_transformation,[status(thm)],[f3584])).
% 20.66/3.38 fof(f14568,plain,(
% 20.66/3.38 ![X0]: (~v2_cat_1(X0)|~l1_cat_1(X0)|~v1_xboole_0(k17_ens_1(X0)))),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f14567])).
% 20.66/3.38 fof(f14792,plain,(
% 20.66/3.38 ![A]: (v1_xboole_0(A)|(![B]: ((~v2_cat_1(B)|~l1_cat_1(B))|(![C]: (~m1_subset_1(C,u1_cat_1(B))|(~r1_tarski(k17_ens_1(B),A)|m2_cat_1(k20_ens_1(B,C),B,k12_ens_1(A))))))))),
% 20.66/3.38 inference(pre_NNF_transformation,[status(thm)],[f3651])).
% 20.66/3.38 fof(f14793,plain,(
% 20.66/3.38 ![X0,X1,X2]: (v1_xboole_0(X0)|~v2_cat_1(X1)|~l1_cat_1(X1)|~m1_subset_1(X2,u1_cat_1(X1))|~r1_tarski(k17_ens_1(X1),X0)|m2_cat_1(k20_ens_1(X1,X2),X1,k12_ens_1(X0)))),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f14792])).
% 20.66/3.38 fof(f15186,plain,(
% 20.66/3.38 ![A]: ((~v2_cat_1(A)|~l1_cat_1(A))|k1_yoneda_1(A)=k12_ens_1(k17_ens_1(A)))),
% 20.66/3.38 inference(pre_NNF_transformation,[status(thm)],[f3800])).
% 20.66/3.38 fof(f15187,plain,(
% 20.66/3.38 ![X0]: (~v2_cat_1(X0)|~l1_cat_1(X0)|k1_yoneda_1(X0)=k12_ens_1(k17_ens_1(X0)))),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f15186])).
% 20.66/3.38 fof(f15190,plain,(
% 20.66/3.38 (?[A]: ((v2_cat_1(A)&l1_cat_1(A))&(?[B]: (m1_subset_1(B,u1_cat_1(A))&~m2_cat_1(k20_ens_1(A,B),A,k1_yoneda_1(A))))))),
% 20.66/3.38 inference(pre_NNF_transformation,[status(thm)],[f3803])).
% 20.66/3.38 fof(f15191,plain,(
% 20.66/3.38 ((v2_cat_1(sK1178_skl)&l1_cat_1(sK1178_skl))&(m1_subset_1(sK1179_skl,u1_cat_1(sK1178_skl))&~m2_cat_1(k20_ens_1(sK1178_skl,sK1179_skl),sK1178_skl,k1_yoneda_1(sK1178_skl))))),
% 20.66/3.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK1178_skl,sK1179_skl]),skolemize(A,sK1178_skl),skolemize(B,sK1179_skl)],[f15190])).
% 20.66/3.38 fof(f15192,plain,(
% 20.66/3.38 v2_cat_1(sK1178_skl)),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f15191])).
% 20.66/3.38 fof(f15193,plain,(
% 20.66/3.38 l1_cat_1(sK1178_skl)),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f15191])).
% 20.66/3.38 fof(f15194,plain,(
% 20.66/3.38 m1_subset_1(sK1179_skl,u1_cat_1(sK1178_skl))),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f15191])).
% 20.66/3.38 fof(f15195,plain,(
% 20.66/3.38 ~m2_cat_1(k20_ens_1(sK1178_skl,sK1179_skl),sK1178_skl,k1_yoneda_1(sK1178_skl))),
% 20.66/3.38 inference(cnf_transformation,[status(thm)],[f15191])).
% 20.66/3.38 fof(f18706,definition,(
% 20.66/3.38 ![X1]: (sQ602_spl <=> (~v2_cat_1(X1)|~l1_cat_1(X1)))),
% 20.66/3.38 introduced(definition,[new_symbols(definition,[sQ602_spl])],[split_symbol_definition])).
% 20.66/3.38 fof(f18707,plain,(
% 20.66/3.38 ![X0]: (~v2_cat_1(X0)|~l1_cat_1(X0)|~sQ602_spl)),
% 20.66/3.38 inference(component_clause,[status(thm)],[f18706])).
% 20.66/3.38 fof(f19309,definition,(
% 20.66/3.38 sQ717_spl <=> (v2_cat_1(sK1178_skl))),
% 20.66/3.38 introduced(definition,[new_symbols(definition,[sQ717_spl])],[split_symbol_definition])).
% 20.66/3.38 fof(f19311,plain,(
% 20.66/3.38 ~v2_cat_1(sK1178_skl)|sQ717_spl),
% 20.66/3.38 inference(component_clause,[status(thm)],[f19309])).
% 20.66/3.38 fof(f19312,definition,(
% 20.66/3.38 sQ718_spl <=> (l1_cat_1(sK1178_skl))),
% 20.66/3.38 introduced(definition,[new_symbols(definition,[sQ718_spl])],[split_symbol_definition])).
% 20.66/3.38 fof(f19314,plain,(
% 20.66/3.38 ~l1_cat_1(sK1178_skl)|sQ718_spl),
% 20.66/3.38 inference(component_clause,[status(thm)],[f19312])).
% 20.66/3.38 fof(f19319,plain,(
% 20.66/3.38 $false|sQ718_spl),
% 20.66/3.38 inference(forward_subsumption_resolution,[status(thm)],[f19314,f15193])).
% 20.66/3.38 fof(f19320,plain,(
% 20.66/3.38 sQ718_spl),
% 20.66/3.38 inference(contradiction_clause,[status(thm)],[f19319])).
% 20.66/3.38 fof(f19321,plain,(
% 20.66/3.38 $false|sQ717_spl),
% 20.66/3.38 inference(forward_subsumption_resolution,[status(thm)],[f19311,f15192])).
% 20.66/3.38 fof(f19322,plain,(
% 20.66/3.38 sQ717_spl),
% 20.66/3.38 inference(contradiction_clause,[status(thm)],[f19321])).
% 20.66/3.38 fof(f19331,definition,(
% 20.66/3.38 sQ721_spl <=> (k1_yoneda_1(sK1178_skl)=k12_ens_1(k17_ens_1(sK1178_skl)))),
% 20.66/3.38 introduced(definition,[new_symbols(definition,[sQ721_spl])],[split_symbol_definition])).
% 20.66/3.38 fof(f19332,plain,(
% 20.66/3.38 k1_yoneda_1(sK1178_skl)=k12_ens_1(k17_ens_1(sK1178_skl))|~sQ721_spl),
% 20.66/3.38 inference(component_clause,[status(thm)],[f19331])).
% 20.66/3.38 fof(f19847,definition,(
% 20.66/3.38 sQ795_spl <=> (v2_cat_1(sK981_skl))),
% 20.66/3.38 introduced(definition,[new_symbols(definition,[sQ795_spl])],[split_symbol_definition])).
% 20.66/3.38 fof(f19849,plain,(
% 20.66/3.38 ~v2_cat_1(sK981_skl)|sQ795_spl),
% 20.66/3.38 inference(component_clause,[status(thm)],[f19847])).
% 20.66/3.38 fof(f19999,plain,(
% 20.66/3.38 $false|sQ795_spl),
% 20.66/3.38 inference(forward_subsumption_resolution,[status(thm)],[f19849,f13041])).
% 20.66/3.38 fof(f20000,plain,(
% 20.66/3.38 sQ795_spl),
% 20.66/3.38 inference(contradiction_clause,[status(thm)],[f19999])).
% 20.66/3.38 fof(f20040,definition,(
% 20.66/3.38 sQ832_spl <=> (v2_cat_1(sK982_skl))),
% 20.66/3.38 introduced(definition,[new_symbols(definition,[sQ832_spl])],[split_symbol_definition])).
% 20.66/3.38 fof(f20042,plain,(
% 20.66/3.38 ~v2_cat_1(sK982_skl)|sQ832_spl),
% 20.66/3.38 inference(component_clause,[status(thm)],[f20040])).
% 20.66/3.38 fof(f20406,definition,(
% 20.66/3.38 sQ906_spl <=> (v2_cat_1(sK1076_skl))),
% 20.66/3.38 introduced(definition,[new_symbols(definition,[sQ906_spl])],[split_symbol_definition])).
% 20.66/3.38 fof(f20408,plain,(
% 20.66/3.38 ~v2_cat_1(sK1076_skl)|sQ906_spl),
% 20.66/3.38 inference(component_clause,[status(thm)],[f20406])).
% 20.66/3.38 fof(f20561,plain,(
% 20.66/3.38 $false|sQ832_spl),
% 20.66/3.38 inference(forward_subsumption_resolution,[status(thm)],[f20042,f13045])).
% 20.66/3.38 fof(f20562,plain,(
% 20.66/3.38 sQ832_spl),
% 20.66/3.38 inference(contradiction_clause,[status(thm)],[f20561])).
% 20.66/3.38 fof(f20563,plain,(
% 20.66/3.38 $false|sQ906_spl),
% 20.66/3.38 inference(forward_subsumption_resolution,[status(thm)],[f20408,f14170])).
% 20.66/3.38 fof(f20564,plain,(
% 20.66/3.38 sQ906_spl),
% 20.66/3.38 inference(contradiction_clause,[status(thm)],[f20563])).
% 20.66/3.38 fof(f20688,plain,(
% 20.66/3.38 ![X0,X1]: (~l1_cat_1(k8_cat_1(X0,X1))|~sQ602_spl)),
% 20.66/3.38 inference(resolution,[status(thm)],[f18707,f13524])).
% 20.66/3.38 fof(f20693,plain,(
% 20.66/3.38 $false|~sQ602_spl),
% 20.66/3.38 inference(forward_subsumption_resolution,[status(thm)],[f20688,f13525])).
% 20.66/3.38 fof(f20694,plain,(
% 20.66/3.38 ~sQ602_spl),
% 20.66/3.38 inference(contradiction_clause,[status(thm)],[f20693])).
% 20.66/3.38 fof(f20707,plain,(
% 20.66/3.38 ~l1_cat_1(sK1178_skl)|k1_yoneda_1(sK1178_skl)=k12_ens_1(k17_ens_1(sK1178_skl))),
% 20.66/3.38 inference(resolution,[status(thm)],[f15187,f15192])).
% 20.66/3.38 fof(f20709,definition,(
% 20.66/3.38 sQ944_spl <=> (l1_cat_1(sK1076_skl))),
% 20.66/3.38 introduced(definition,[new_symbols(definition,[sQ944_spl])],[split_symbol_definition])).
% 20.66/3.38 fof(f20711,plain,(
% 20.66/3.38 ~l1_cat_1(sK1076_skl)|sQ944_spl),
% 20.66/3.38 inference(component_clause,[status(thm)],[f20709])).
% 20.66/3.38 fof(f20713,definition,(
% 20.66/3.38 sQ945_spl <=> (l1_cat_1(sK982_skl))),
% 20.66/3.38 introduced(definition,[new_symbols(definition,[sQ945_spl])],[split_symbol_definition])).
% 20.66/3.38 fof(f20715,plain,(
% 20.66/3.38 ~l1_cat_1(sK982_skl)|sQ945_spl),
% 20.66/3.38 inference(component_clause,[status(thm)],[f20713])).
% 20.66/3.38 fof(f20717,definition,(
% 20.66/3.38 sQ946_spl <=> (l1_cat_1(sK981_skl))),
% 20.66/3.38 introduced(definition,[new_symbols(definition,[sQ946_spl])],[split_symbol_definition])).
% 20.66/3.38 fof(f20719,plain,(
% 20.66/3.38 ~l1_cat_1(sK981_skl)|sQ946_spl),
% 20.66/3.38 inference(component_clause,[status(thm)],[f20717])).
% 20.66/3.38 fof(f20721,plain,(
% 20.66/3.38 ~sQ718_spl|sQ721_spl),
% 20.66/3.38 inference(split_clause,[status(thm)],[f20707,f19312,f19331])).
% 20.66/3.38 fof(f20722,plain,(
% 20.66/3.38 $false|sQ946_spl),
% 20.66/3.38 inference(forward_subsumption_resolution,[status(thm)],[f20719,f13040])).
% 20.66/3.38 fof(f20723,plain,(
% 20.66/3.38 sQ946_spl),
% 20.66/3.38 inference(contradiction_clause,[status(thm)],[f20722])).
% 20.66/3.38 fof(f20724,plain,(
% 20.66/3.38 $false|sQ945_spl),
% 20.66/3.38 inference(forward_subsumption_resolution,[status(thm)],[f20715,f13043])).
% 20.66/3.38 fof(f20725,plain,(
% 20.66/3.38 sQ945_spl),
% 20.66/3.38 inference(contradiction_clause,[status(thm)],[f20724])).
% 20.66/3.38 fof(f20726,plain,(
% 20.66/3.38 $false|sQ944_spl),
% 20.66/3.38 inference(forward_subsumption_resolution,[status(thm)],[f20711,f14169])).
% 20.66/3.38 fof(f20727,plain,(
% 20.66/3.38 sQ944_spl),
% 20.66/3.38 inference(contradiction_clause,[status(thm)],[f20726])).
% 20.66/3.38 fof(f20904,plain,(
% 20.66/3.38 ![X0,X1]: (v1_xboole_0(k17_ens_1(X0))|~v2_cat_1(X0)|~l1_cat_1(X0)|~m1_subset_1(X1,u1_cat_1(X0))|m2_cat_1(k20_ens_1(X0,X1),X0,k12_ens_1(k17_ens_1(X0))))),
% 20.66/3.38 inference(resolution,[status(thm)],[f3880,f14793])).
% 20.66/3.38 fof(f20916,plain,(
% 20.66/3.38 v1_xboole_0(k17_ens_1(sK1178_skl))|~v2_cat_1(sK1178_skl)|~l1_cat_1(sK1178_skl)|m2_cat_1(k20_ens_1(sK1178_skl,sK1179_skl),sK1178_skl,k12_ens_1(k17_ens_1(sK1178_skl)))),
% 20.66/3.38 inference(resolution,[status(thm)],[f20904,f15194])).
% 20.66/3.38 fof(f20917,definition,(
% 20.66/3.38 sQ947_spl <=> (v1_xboole_0(k17_ens_1(sK1178_skl)))),
% 20.66/3.38 introduced(definition,[new_symbols(definition,[sQ947_spl])],[split_symbol_definition])).
% 20.66/3.38 fof(f20918,plain,(
% 20.66/3.38 v1_xboole_0(k17_ens_1(sK1178_skl))|~sQ947_spl),
% 20.66/3.38 inference(component_clause,[status(thm)],[f20917])).
% 20.66/3.38 fof(f20920,definition,(
% 20.66/3.38 sQ948_spl <=> (m2_cat_1(k20_ens_1(sK1178_skl,sK1179_skl),sK1178_skl,k12_ens_1(k17_ens_1(sK1178_skl))))),
% 20.66/3.38 introduced(definition,[new_symbols(definition,[sQ948_spl])],[split_symbol_definition])).
% 20.66/3.38 fof(f20921,plain,(
% 20.66/3.38 m2_cat_1(k20_ens_1(sK1178_skl,sK1179_skl),sK1178_skl,k12_ens_1(k17_ens_1(sK1178_skl)))|~sQ948_spl),
% 20.66/3.38 inference(component_clause,[status(thm)],[f20920])).
% 20.66/3.38 fof(f20923,plain,(
% 20.66/3.38 sQ947_spl|~sQ717_spl|~sQ718_spl|sQ948_spl),
% 20.66/3.38 inference(split_clause,[status(thm)],[f20916,f20917,f19309,f19312,f20920])).
% 20.66/3.38 fof(f20924,plain,(
% 20.66/3.38 m2_cat_1(k20_ens_1(sK1178_skl,sK1179_skl),sK1178_skl,k1_yoneda_1(sK1178_skl))|~sQ721_spl|~sQ948_spl),
% 20.66/3.38 inference(forward_demodulation,[status(thm)],[f19332,f20921])).
% 20.66/3.38 fof(f20925,plain,(
% 20.66/3.38 $false|~sQ721_spl|~sQ948_spl),
% 20.66/3.44 inference(forward_subsumption_resolution,[status(thm)],[f20924,f15195])).
% 20.66/3.44 fof(f20926,plain,(
% 20.66/3.44 ~sQ721_spl|~sQ948_spl),
% 20.66/3.44 inference(contradiction_clause,[status(thm)],[f20925])).
% 20.66/3.44 fof(f22855,plain,(
% 20.66/3.44 ~v2_cat_1(sK1178_skl)|~l1_cat_1(sK1178_skl)|~sQ947_spl),
% 20.66/3.44 inference(resolution,[status(thm)],[f14568,f20918])).
% 20.66/3.44 fof(f22856,plain,(
% 20.66/3.44 ~sQ717_spl|~sQ718_spl|~sQ947_spl),
% 20.66/3.44 inference(split_clause,[status(thm)],[f22855,f19309,f19312,f20917])).
% 20.66/3.44 fof(f22857,plain,(
% 20.66/3.44 $false),
% 20.66/3.44 inference(sat_refutation,[status(thm)],[f19320,f19322,f20000,f20562,f20564,f20694,f20721,f20723,f20725,f20727,f20923,f20926,f22856])).
% 20.66/3.44 % SZS output end CNFRefutation for theBenchmark.p
% 9.64/3.47 % Elapsed time: 3.106948 seconds
% 9.64/3.47 % CPU time: 21.351641 seconds
% 9.64/3.47 % Total memory used: 921.477 MB
% 9.64/3.47 % Net memory used: 901.545 MB
%------------------------------------------------------------------------------