%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CAT033+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 : n017.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 122.54s 17.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CAT033+3 : 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.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 13:56:14 UTC 2026
% 0.10/0.36 % CPUTime :
% 2.46/2.75 % Drodi V4.1.1
% 122.54/17.94 % Refutation found
% 122.54/17.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 122.54/17.94 % SZS output start CNFRefutation for theBenchmark
% 122.54/17.94 fof(f18,axiom,(
% 122.54/17.94 (! [A,B] : r1_tarski(A,A) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f24,axiom,(
% 122.54/17.94 v1_xboole_0(k1_xboole_0) ),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f33,axiom,(
% 122.54/17.94 (! [A] :( v1_xboole_0(A)<=> A = k1_xboole_0 ) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f71,axiom,(
% 122.54/17.94 (! [A] : r1_tarski(k1_xboole_0,A) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f680,axiom,(
% 122.54/17.94 (? [A] :( v1_xboole_0(A)& v1_relat_1(A) ) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f6446,axiom,(
% 122.54/17.94 (? [A] :( l1_cat_1(A)& v2_cat_1(A) ) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f6447,axiom,(
% 122.54/17.94 (? [A] :( l1_cat_1(A)& v1_cat_1(A)& v2_cat_1(A) ) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f6620,axiom,(
% 122.54/17.94 (! [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)) ) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f10443,axiom,(
% 122.54/17.94 (? [A] :( l1_cat_1(A)& v2_cat_1(A)& v2_nattra_1(A) ) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f10621,axiom,(
% 122.54/17.94 (! [A] :( ( v2_cat_1(A)& l1_cat_1(A) )=> ~ v1_xboole_0(k17_ens_1(A)) ) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f10688,axiom,(
% 122.54/17.94 (! [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)) ) ) )) )) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f13687,axiom,(
% 122.54/17.94 (? [A] :( l1_cat_1(A)& v1_cat_1(A)& v2_cat_1(A)& v1_cat_5(A) ) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f13690,axiom,(
% 122.54/17.94 (? [A] :( l1_cat_1(A)& v1_cat_1(A)& v2_cat_1(A)& v1_cat_5(A)& v3_cat_5(A) ) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f13692,axiom,(
% 122.54/17.94 (? [A] :( l1_cat_1(A)& v1_cat_1(A)& v2_cat_1(A)& v1_cat_5(A)& v3_cat_5(A)& v4_cat_5(A) ) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f15993,axiom,(
% 122.54/17.94 (? [A] :( ~ v1_xboole_0(A)& v1_relat_1(A)& v1_funct_1(A)& v5_seqm_3(A)& v2_pralg_1(A) ) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f16907,axiom,(
% 122.54/17.94 (! [A] :( ( v2_cat_1(A)& l1_cat_1(A) )=> k1_yoneda_1(A) = k12_ens_1(k17_ens_1(A)) ) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f16909,conjecture,(
% 122.54/17.94 (! [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)) ) )) )),
% 122.54/17.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 122.54/17.94 fof(f16910,negated_conjecture,(
% 122.54/17.94 ~((! [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)) ) )) ))),
% 122.54/17.94 inference(negated_conjecture,[status(cth)],[f16909])).
% 122.54/17.94 fof(f16986,plain,(
% 122.54/17.94 ![A]: r1_tarski(A,A)),
% 122.54/17.94 inference(miniscoping,[status(thm)],[f18])).
% 122.54/17.94 fof(f16987,plain,(
% 122.54/17.94 ![X0]: (r1_tarski(X0,X0))),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f16986])).
% 122.54/17.94 fof(f16989,plain,(
% 122.54/17.94 v1_xboole_0(k1_xboole_0)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f24])).
% 122.54/17.94 fof(f17032,plain,(
% 122.54/17.94 ![A]: ((~v1_xboole_0(A)|A=k1_xboole_0)&(v1_xboole_0(A)|~A=k1_xboole_0))),
% 122.54/17.94 inference(NNF_transformation,[status(thm)],[f33])).
% 122.54/17.94 fof(f17033,plain,(
% 122.54/17.94 (![A]: (~v1_xboole_0(A)|A=k1_xboole_0))&(![A]: (v1_xboole_0(A)|~A=k1_xboole_0))),
% 122.54/17.94 inference(miniscoping,[status(thm)],[f17032])).
% 122.54/17.94 fof(f17034,plain,(
% 122.54/17.94 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f17033])).
% 122.54/17.94 fof(f17139,plain,(
% 122.54/17.94 ![X0]: (r1_tarski(k1_xboole_0,X0))),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f71])).
% 122.54/17.94 fof(f18387,plain,(
% 122.54/17.94 (v1_xboole_0(sK124_skl)&v1_relat_1(sK124_skl))),
% 122.54/17.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK124_skl]),skolemize(A,sK124_skl)],[f680])).
% 122.54/17.94 fof(f18389,plain,(
% 122.54/17.94 v1_relat_1(sK124_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f18387])).
% 122.54/17.94 fof(f36687,plain,(
% 122.54/17.94 (l1_cat_1(sK1864_skl)&v2_cat_1(sK1864_skl))),
% 122.54/17.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK1864_skl]),skolemize(A,sK1864_skl)],[f6446])).
% 122.54/17.94 fof(f36688,plain,(
% 122.54/17.94 l1_cat_1(sK1864_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f36687])).
% 122.54/17.94 fof(f36689,plain,(
% 122.54/17.94 v2_cat_1(sK1864_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f36687])).
% 122.54/17.94 fof(f36690,plain,(
% 122.54/17.94 ((l1_cat_1(sK1865_skl)&v1_cat_1(sK1865_skl))&v2_cat_1(sK1865_skl))),
% 122.54/17.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK1865_skl]),skolemize(A,sK1865_skl)],[f6447])).
% 122.54/17.94 fof(f36691,plain,(
% 122.54/17.94 l1_cat_1(sK1865_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f36690])).
% 122.54/17.94 fof(f36693,plain,(
% 122.54/17.94 v2_cat_1(sK1865_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f36690])).
% 122.54/17.94 fof(f37170,plain,(
% 122.54/17.94 ((![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)))),
% 122.54/17.94 inference(miniscoping,[status(thm)],[f6620])).
% 122.54/17.94 fof(f37172,plain,(
% 122.54/17.94 ![X0,X1]: (v2_cat_1(k8_cat_1(X0,X1)))),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f37170])).
% 122.54/17.94 fof(f37173,plain,(
% 122.54/17.94 ![X0,X1]: (l1_cat_1(k8_cat_1(X0,X1)))),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f37170])).
% 122.54/17.94 fof(f48188,plain,(
% 122.54/17.94 ((l1_cat_1(sK2824_skl)&v2_cat_1(sK2824_skl))&v2_nattra_1(sK2824_skl))),
% 122.54/17.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK2824_skl]),skolemize(A,sK2824_skl)],[f10443])).
% 122.54/17.94 fof(f48189,plain,(
% 122.54/17.94 l1_cat_1(sK2824_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f48188])).
% 122.54/17.94 fof(f48190,plain,(
% 122.54/17.94 v2_cat_1(sK2824_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f48188])).
% 122.54/17.94 fof(f48832,plain,(
% 122.54/17.94 ![A]: ((~v2_cat_1(A)|~l1_cat_1(A))|~v1_xboole_0(k17_ens_1(A)))),
% 122.54/17.94 inference(pre_NNF_transformation,[status(thm)],[f10621])).
% 122.54/17.94 fof(f48833,plain,(
% 122.54/17.94 ![X0]: (~v2_cat_1(X0)|~l1_cat_1(X0)|~v1_xboole_0(k17_ens_1(X0)))),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f48832])).
% 122.54/17.94 fof(f49057,plain,(
% 122.54/17.94 ![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))))))))),
% 122.54/17.94 inference(pre_NNF_transformation,[status(thm)],[f10688])).
% 122.54/17.94 fof(f49058,plain,(
% 122.54/17.94 ![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)))),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f49057])).
% 122.54/17.94 fof(f61334,plain,(
% 122.54/17.94 (((l1_cat_1(sK4001_skl)&v1_cat_1(sK4001_skl))&v2_cat_1(sK4001_skl))&v1_cat_5(sK4001_skl))),
% 122.54/17.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK4001_skl]),skolemize(A,sK4001_skl)],[f13687])).
% 122.54/17.94 fof(f61335,plain,(
% 122.54/17.94 l1_cat_1(sK4001_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f61334])).
% 122.54/17.94 fof(f61337,plain,(
% 122.54/17.94 v2_cat_1(sK4001_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f61334])).
% 122.54/17.94 fof(f61345,plain,(
% 122.54/17.94 ((((l1_cat_1(sK4003_skl)&v1_cat_1(sK4003_skl))&v2_cat_1(sK4003_skl))&v1_cat_5(sK4003_skl))&v3_cat_5(sK4003_skl))),
% 122.54/17.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK4003_skl]),skolemize(A,sK4003_skl)],[f13690])).
% 122.54/17.94 fof(f61346,plain,(
% 122.54/17.94 l1_cat_1(sK4003_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f61345])).
% 122.54/17.94 fof(f61348,plain,(
% 122.54/17.94 v2_cat_1(sK4003_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f61345])).
% 122.54/17.94 fof(f61353,plain,(
% 122.54/17.94 (((((l1_cat_1(sK4004_skl)&v1_cat_1(sK4004_skl))&v2_cat_1(sK4004_skl))&v1_cat_5(sK4004_skl))&v3_cat_5(sK4004_skl))&v4_cat_5(sK4004_skl))),
% 122.54/17.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK4004_skl]),skolemize(A,sK4004_skl)],[f13692])).
% 122.54/17.94 fof(f61354,plain,(
% 122.54/17.94 l1_cat_1(sK4004_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f61353])).
% 122.54/17.94 fof(f61356,plain,(
% 122.54/17.94 v2_cat_1(sK4004_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f61353])).
% 122.54/17.94 fof(f71205,plain,(
% 122.54/17.94 ((((~v1_xboole_0(sK5025_skl)&v1_relat_1(sK5025_skl))&v1_funct_1(sK5025_skl))&v5_seqm_3(sK5025_skl))&v2_pralg_1(sK5025_skl))),
% 122.54/17.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK5025_skl]),skolemize(A,sK5025_skl)],[f15993])).
% 122.54/17.94 fof(f71207,plain,(
% 122.54/17.94 v1_relat_1(sK5025_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f71205])).
% 122.54/17.94 fof(f71208,plain,(
% 122.54/17.94 v1_funct_1(sK5025_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f71205])).
% 122.54/17.94 fof(f75788,plain,(
% 122.54/17.94 ![A]: ((~v2_cat_1(A)|~l1_cat_1(A))|k1_yoneda_1(A)=k12_ens_1(k17_ens_1(A)))),
% 122.54/17.94 inference(pre_NNF_transformation,[status(thm)],[f16907])).
% 122.54/17.94 fof(f75789,plain,(
% 122.54/17.94 ![X0]: (~v2_cat_1(X0)|~l1_cat_1(X0)|k1_yoneda_1(X0)=k12_ens_1(k17_ens_1(X0)))),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f75788])).
% 122.54/17.94 fof(f75792,plain,(
% 122.54/17.94 (?[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))))))),
% 122.54/17.94 inference(pre_NNF_transformation,[status(thm)],[f16910])).
% 122.54/17.94 fof(f75793,plain,(
% 122.54/17.94 ((v2_cat_1(sK5420_skl)&l1_cat_1(sK5420_skl))&(m1_subset_1(sK5421_skl,u1_cat_1(sK5420_skl))&~m2_cat_1(k20_ens_1(sK5420_skl,sK5421_skl),sK5420_skl,k1_yoneda_1(sK5420_skl))))),
% 122.54/17.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK5420_skl,sK5421_skl]),skolemize(A,sK5420_skl),skolemize(B,sK5421_skl)],[f75792])).
% 122.54/17.94 fof(f75794,plain,(
% 122.54/17.94 v2_cat_1(sK5420_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f75793])).
% 122.54/17.94 fof(f75795,plain,(
% 122.54/17.94 l1_cat_1(sK5420_skl)),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f75793])).
% 122.54/17.94 fof(f75796,plain,(
% 122.54/17.94 m1_subset_1(sK5421_skl,u1_cat_1(sK5420_skl))),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f75793])).
% 122.54/17.94 fof(f75797,plain,(
% 122.54/17.94 ~m2_cat_1(k20_ens_1(sK5420_skl,sK5421_skl),sK5420_skl,k1_yoneda_1(sK5420_skl))),
% 122.54/17.94 inference(cnf_transformation,[status(thm)],[f75793])).
% 122.54/17.94 fof(f80190,definition,(
% 122.54/17.94 ![X1]: (sQ84_spl <=> (~v1_relat_1(X1)|~v1_funct_1(X1)))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f80191,plain,(
% 122.54/17.94 ![X0]: (~v1_relat_1(X0)|~v1_funct_1(X0)|~sQ84_spl)),
% 122.54/17.94 inference(component_clause,[status(thm)],[f80190])).
% 122.54/17.94 fof(f82718,definition,(
% 122.54/17.94 ![X1]: (sQ749_spl <=> (~v1_relat_1(X1)))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ749_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f82719,plain,(
% 122.54/17.94 ![X0]: (~v1_relat_1(X0)|~sQ749_spl)),
% 122.54/17.94 inference(component_clause,[status(thm)],[f82718])).
% 122.54/17.94 fof(f83340,definition,(
% 122.54/17.94 ![X1]: (sQ914_spl <=> (~v2_cat_1(X1)|~l1_cat_1(X1)))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ914_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f83341,plain,(
% 122.54/17.94 ![X0]: (~v2_cat_1(X0)|~l1_cat_1(X0)|~sQ914_spl)),
% 122.54/17.94 inference(component_clause,[status(thm)],[f83340])).
% 122.54/17.94 fof(f88947,definition,(
% 122.54/17.94 sQ1361_spl <=> (v2_cat_1(sK5420_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ1361_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f88949,plain,(
% 122.54/17.94 ~v2_cat_1(sK5420_skl)|sQ1361_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f88947])).
% 122.54/17.94 fof(f88950,definition,(
% 122.54/17.94 sQ1362_spl <=> (l1_cat_1(sK5420_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ1362_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f88952,plain,(
% 122.54/17.94 ~l1_cat_1(sK5420_skl)|sQ1362_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f88950])).
% 122.54/17.94 fof(f88957,plain,(
% 122.54/17.94 $false|sQ1362_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f88952,f75795])).
% 122.54/17.94 fof(f88958,plain,(
% 122.54/17.94 sQ1362_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f88957])).
% 122.54/17.94 fof(f88959,plain,(
% 122.54/17.94 $false|sQ1361_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f88949,f75794])).
% 122.54/17.94 fof(f88960,plain,(
% 122.54/17.94 sQ1361_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f88959])).
% 122.54/17.94 fof(f88962,plain,(
% 122.54/17.94 ~l1_cat_1(sK5420_skl)|k1_yoneda_1(sK5420_skl)=k12_ens_1(k17_ens_1(sK5420_skl))),
% 122.54/17.94 inference(resolution,[status(thm)],[f75789,f75794])).
% 122.54/17.94 fof(f88964,definition,(
% 122.54/17.94 sQ1364_spl <=> (k1_yoneda_1(sK5420_skl)=k12_ens_1(k17_ens_1(sK5420_skl)))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ1364_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f88965,plain,(
% 122.54/17.94 k1_yoneda_1(sK5420_skl)=k12_ens_1(k17_ens_1(sK5420_skl))|~sQ1364_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f88964])).
% 122.54/17.94 fof(f88967,plain,(
% 122.54/17.94 ~sQ1362_spl|sQ1364_spl),
% 122.54/17.94 inference(split_clause,[status(thm)],[f88962,f88950,f88964])).
% 122.54/17.94 fof(f89139,plain,(
% 122.54/17.94 $false|~sQ749_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f18389,f82719])).
% 122.54/17.94 fof(f89140,plain,(
% 122.54/17.94 ~sQ749_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f89139])).
% 122.54/17.94 fof(f89811,definition,(
% 122.54/17.94 sQ1461_spl <=> (l1_cat_1(sK1864_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ1461_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f89813,plain,(
% 122.54/17.94 ~l1_cat_1(sK1864_skl)|sQ1461_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f89811])).
% 122.54/17.94 fof(f90195,plain,(
% 122.54/17.94 $false|sQ1461_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f89813,f36688])).
% 122.54/17.94 fof(f90196,plain,(
% 122.54/17.94 sQ1461_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f90195])).
% 122.54/17.94 fof(f90296,definition,(
% 122.54/17.94 sQ1558_spl <=> (l1_cat_1(sK1865_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ1558_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f90298,plain,(
% 122.54/17.94 ~l1_cat_1(sK1865_skl)|sQ1558_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f90296])).
% 122.54/17.94 fof(f90680,plain,(
% 122.54/17.94 $false|sQ1558_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f90298,f36691])).
% 122.54/17.94 fof(f90681,plain,(
% 122.54/17.94 sQ1558_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f90680])).
% 122.54/17.94 fof(f90687,plain,(
% 122.54/17.94 ![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))))),
% 122.54/17.94 inference(resolution,[status(thm)],[f16987,f49058])).
% 122.54/17.94 fof(f90707,plain,(
% 122.54/17.94 v1_xboole_0(k17_ens_1(sK5420_skl))|~v2_cat_1(sK5420_skl)|~l1_cat_1(sK5420_skl)|m2_cat_1(k20_ens_1(sK5420_skl,sK5421_skl),sK5420_skl,k12_ens_1(k17_ens_1(sK5420_skl)))),
% 122.54/17.94 inference(resolution,[status(thm)],[f90687,f75796])).
% 122.54/17.94 fof(f90708,definition,(
% 122.54/17.94 sQ1654_spl <=> (v1_xboole_0(k17_ens_1(sK5420_skl)))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ1654_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f90709,plain,(
% 122.54/17.94 v1_xboole_0(k17_ens_1(sK5420_skl))|~sQ1654_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f90708])).
% 122.54/17.94 fof(f90711,definition,(
% 122.54/17.94 sQ1655_spl <=> (m2_cat_1(k20_ens_1(sK5420_skl,sK5421_skl),sK5420_skl,k12_ens_1(k17_ens_1(sK5420_skl))))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ1655_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f90712,plain,(
% 122.54/17.94 m2_cat_1(k20_ens_1(sK5420_skl,sK5421_skl),sK5420_skl,k12_ens_1(k17_ens_1(sK5420_skl)))|~sQ1655_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f90711])).
% 122.54/17.94 fof(f90714,plain,(
% 122.54/17.94 sQ1654_spl|~sQ1361_spl|~sQ1362_spl|sQ1655_spl),
% 122.54/17.94 inference(split_clause,[status(thm)],[f90707,f90708,f88947,f88950,f90711])).
% 122.54/17.94 fof(f90715,plain,(
% 122.54/17.94 m2_cat_1(k20_ens_1(sK5420_skl,sK5421_skl),sK5420_skl,k1_yoneda_1(sK5420_skl))|~sQ1364_spl|~sQ1655_spl),
% 122.54/17.94 inference(forward_demodulation,[status(thm)],[f88965,f90712])).
% 122.54/17.94 fof(f90716,plain,(
% 122.54/17.94 $false|~sQ1364_spl|~sQ1655_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f90715,f75797])).
% 122.54/17.94 fof(f90717,plain,(
% 122.54/17.94 ~sQ1364_spl|~sQ1655_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f90716])).
% 122.54/17.94 fof(f90818,definition,(
% 122.54/17.94 sQ1657_spl <=> (l1_cat_1(sK2824_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ1657_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f90820,plain,(
% 122.54/17.94 ~l1_cat_1(sK2824_skl)|sQ1657_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f90818])).
% 122.54/17.94 fof(f91202,plain,(
% 122.54/17.94 $false|sQ1657_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f90820,f48189])).
% 122.54/17.94 fof(f91203,plain,(
% 122.54/17.94 sQ1657_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f91202])).
% 122.54/17.94 fof(f91331,definition,(
% 122.54/17.94 sQ1754_spl <=> (l1_cat_1(sK4001_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ1754_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f91333,plain,(
% 122.54/17.94 ~l1_cat_1(sK4001_skl)|sQ1754_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f91331])).
% 122.54/17.94 fof(f91715,plain,(
% 122.54/17.94 $false|sQ1754_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f91333,f61335])).
% 122.54/17.94 fof(f91716,plain,(
% 122.54/17.94 sQ1754_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f91715])).
% 122.54/17.94 fof(f91835,definition,(
% 122.54/17.94 sQ1851_spl <=> (l1_cat_1(sK4003_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ1851_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f91837,plain,(
% 122.54/17.94 ~l1_cat_1(sK4003_skl)|sQ1851_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f91835])).
% 122.54/17.94 fof(f92219,plain,(
% 122.54/17.94 $false|sQ1851_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f91837,f61346])).
% 122.54/17.94 fof(f92220,plain,(
% 122.54/17.94 sQ1851_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f92219])).
% 122.54/17.94 fof(f92320,definition,(
% 122.54/17.94 sQ1948_spl <=> (l1_cat_1(sK4004_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ1948_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f92322,plain,(
% 122.54/17.94 ~l1_cat_1(sK4004_skl)|sQ1948_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f92320])).
% 122.54/17.94 fof(f92704,plain,(
% 122.54/17.94 $false|sQ1948_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f92322,f61354])).
% 122.54/17.94 fof(f92705,plain,(
% 122.54/17.94 sQ1948_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f92704])).
% 122.54/17.94 fof(f93485,plain,(
% 122.54/17.94 k17_ens_1(sK5420_skl)=k1_xboole_0|~sQ1654_spl),
% 122.54/17.94 inference(resolution,[status(thm)],[f17034,f90709])).
% 122.54/17.94 fof(f93495,plain,(
% 122.54/17.94 k1_yoneda_1(sK5420_skl)=k12_ens_1(k1_xboole_0)|~sQ1654_spl|~sQ1364_spl),
% 122.54/17.94 inference(backward_demodulation,[status(thm)],[f93485,f88965])).
% 122.54/17.94 fof(f93498,plain,(
% 122.54/17.94 ![X0,X1]: (v1_xboole_0(X0)|~v2_cat_1(sK5420_skl)|~l1_cat_1(sK5420_skl)|~m1_subset_1(X1,u1_cat_1(sK5420_skl))|~r1_tarski(k1_xboole_0,X0)|m2_cat_1(k20_ens_1(sK5420_skl,X1),sK5420_skl,k12_ens_1(X0))|~sQ1654_spl)),
% 122.54/17.94 inference(paramodulation,[status(thm)],[f93485,f49058])).
% 122.54/17.94 fof(f93507,definition,(
% 122.54/17.94 ![X0,X1]: (sQ2142_spl <=> (v1_xboole_0(X0)|~m1_subset_1(X1,u1_cat_1(sK5420_skl))|~r1_tarski(k1_xboole_0,X0)|m2_cat_1(k20_ens_1(sK5420_skl,X1),sK5420_skl,k12_ens_1(X0))))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ2142_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f93508,plain,(
% 122.54/17.94 ![X0,X1]: (v1_xboole_0(X0)|~m1_subset_1(X1,u1_cat_1(sK5420_skl))|~r1_tarski(k1_xboole_0,X0)|m2_cat_1(k20_ens_1(sK5420_skl,X1),sK5420_skl,k12_ens_1(X0))|~sQ2142_spl)),
% 122.54/17.94 inference(component_clause,[status(thm)],[f93507])).
% 122.54/17.94 fof(f93510,plain,(
% 122.54/17.94 sQ2142_spl|~sQ1361_spl|~sQ1362_spl|~sQ1654_spl),
% 122.54/17.94 inference(split_clause,[status(thm)],[f93498,f93507,f88947,f88950,f90708])).
% 122.54/17.94 fof(f93606,plain,(
% 122.54/17.94 ~m2_cat_1(k20_ens_1(sK5420_skl,sK5421_skl),sK5420_skl,k12_ens_1(k1_xboole_0))|~sQ1654_spl|~sQ1364_spl),
% 122.54/17.94 inference(backward_demodulation,[status(thm)],[f93495,f75797])).
% 122.54/17.94 fof(f94234,plain,(
% 122.54/17.94 ![X0]: (v1_xboole_0(X0)|~r1_tarski(k1_xboole_0,X0)|m2_cat_1(k20_ens_1(sK5420_skl,sK5421_skl),sK5420_skl,k12_ens_1(X0))|~sQ2142_spl)),
% 122.54/17.94 inference(resolution,[status(thm)],[f93508,f75796])).
% 122.54/17.94 fof(f94240,plain,(
% 122.54/17.94 v1_xboole_0(k1_xboole_0)|m2_cat_1(k20_ens_1(sK5420_skl,sK5421_skl),sK5420_skl,k12_ens_1(k1_xboole_0))|~sQ2142_spl),
% 122.54/17.94 inference(resolution,[status(thm)],[f94234,f16987])).
% 122.54/17.94 fof(f94241,definition,(
% 122.54/17.94 sQ2243_spl <=> (v1_xboole_0(k1_xboole_0))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ2243_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f94244,definition,(
% 122.54/17.94 sQ2244_spl <=> (m2_cat_1(k20_ens_1(sK5420_skl,sK5421_skl),sK5420_skl,k12_ens_1(k1_xboole_0)))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ2244_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f94245,plain,(
% 122.54/17.94 m2_cat_1(k20_ens_1(sK5420_skl,sK5421_skl),sK5420_skl,k12_ens_1(k1_xboole_0))|~sQ2244_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f94244])).
% 122.54/17.94 fof(f94247,plain,(
% 122.54/17.94 sQ2243_spl|sQ2244_spl|~sQ2142_spl),
% 122.54/17.94 inference(split_clause,[status(thm)],[f94240,f94241,f94244,f93507])).
% 122.54/17.94 fof(f94248,plain,(
% 122.54/17.94 $false|~sQ1654_spl|~sQ1364_spl|~sQ2244_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f94245,f93606])).
% 122.54/17.94 fof(f94249,plain,(
% 122.54/17.94 ~sQ1654_spl|~sQ1364_spl|~sQ2244_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f94248])).
% 122.54/17.94 fof(f94605,plain,(
% 122.54/17.94 ~v1_funct_1(sK5025_skl)|~sQ84_spl),
% 122.54/17.94 inference(resolution,[status(thm)],[f80191,f71207])).
% 122.54/17.94 fof(f94677,plain,(
% 122.54/17.94 $false|~sQ84_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f94605,f71208])).
% 122.54/17.94 fof(f94678,plain,(
% 122.54/17.94 ~sQ84_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f94677])).
% 122.54/17.94 fof(f94731,plain,(
% 122.54/17.94 ![X0,X1]: (~l1_cat_1(k8_cat_1(X0,X1))|~sQ914_spl)),
% 122.54/17.94 inference(resolution,[status(thm)],[f83341,f37172])).
% 122.54/17.94 fof(f94741,plain,(
% 122.54/17.94 $false|~sQ914_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f94731,f37173])).
% 122.54/17.94 fof(f94742,plain,(
% 122.54/17.94 ~sQ914_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f94741])).
% 122.54/17.94 fof(f95497,definition,(
% 122.54/17.94 ![X0]: (sQ2270_spl <=> (~v1_xboole_0(X0)))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ2270_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f95498,plain,(
% 122.54/17.94 ![X0]: (~v1_xboole_0(X0)|~sQ2270_spl)),
% 122.54/17.94 inference(component_clause,[status(thm)],[f95497])).
% 122.54/17.94 fof(f95654,plain,(
% 122.54/17.94 $false|~sQ2270_spl),
% 122.54/17.94 inference(backward_subsumption_resolution,[status(thm)],[f16989,f95498])).
% 122.54/17.94 fof(f95655,plain,(
% 122.54/17.94 ~sQ2270_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f95654])).
% 122.54/17.94 fof(f98733,definition,(
% 122.54/17.94 sQ3005_spl <=> (v2_cat_1(sK4004_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ3005_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f98735,plain,(
% 122.54/17.94 ~v2_cat_1(sK4004_skl)|sQ3005_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f98733])).
% 122.54/17.94 fof(f98744,plain,(
% 122.54/17.94 $false|sQ3005_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f98735,f61356])).
% 122.54/17.94 fof(f98745,plain,(
% 122.54/17.94 sQ3005_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f98744])).
% 122.54/17.94 fof(f98750,definition,(
% 122.54/17.94 sQ3008_spl <=> (v2_cat_1(sK4003_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ3008_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f98752,plain,(
% 122.54/17.94 ~v2_cat_1(sK4003_skl)|sQ3008_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f98750])).
% 122.54/17.94 fof(f98761,plain,(
% 122.54/17.94 $false|sQ3008_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f98752,f61348])).
% 122.54/17.94 fof(f98762,plain,(
% 122.54/17.94 sQ3008_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f98761])).
% 122.54/17.94 fof(f98767,definition,(
% 122.54/17.94 sQ3011_spl <=> (v2_cat_1(sK4001_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ3011_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f98769,plain,(
% 122.54/17.94 ~v2_cat_1(sK4001_skl)|sQ3011_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f98767])).
% 122.54/17.94 fof(f98778,plain,(
% 122.54/17.94 $false|sQ3011_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f98769,f61337])).
% 122.54/17.94 fof(f98779,plain,(
% 122.54/17.94 sQ3011_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f98778])).
% 122.54/17.94 fof(f98784,definition,(
% 122.54/17.94 sQ3014_spl <=> (v2_cat_1(sK2824_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ3014_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f98786,plain,(
% 122.54/17.94 ~v2_cat_1(sK2824_skl)|sQ3014_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f98784])).
% 122.54/17.94 fof(f98795,plain,(
% 122.54/17.94 $false|sQ3014_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f98786,f48190])).
% 122.54/17.94 fof(f98796,plain,(
% 122.54/17.94 sQ3014_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f98795])).
% 122.54/17.94 fof(f98801,definition,(
% 122.54/17.94 sQ3017_spl <=> (v2_cat_1(sK1865_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ3017_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f98803,plain,(
% 122.54/17.94 ~v2_cat_1(sK1865_skl)|sQ3017_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f98801])).
% 122.54/17.94 fof(f98812,plain,(
% 122.54/17.94 $false|sQ3017_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f98803,f36693])).
% 122.54/17.94 fof(f98813,plain,(
% 122.54/17.94 sQ3017_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f98812])).
% 122.54/17.94 fof(f98818,definition,(
% 122.54/17.94 sQ3020_spl <=> (v2_cat_1(sK1864_skl))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ3020_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f98820,plain,(
% 122.54/17.94 ~v2_cat_1(sK1864_skl)|sQ3020_spl),
% 122.54/17.94 inference(component_clause,[status(thm)],[f98818])).
% 122.54/17.94 fof(f98829,plain,(
% 122.54/17.94 $false|sQ3020_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f98820,f36689])).
% 122.54/17.94 fof(f98830,plain,(
% 122.54/17.94 sQ3020_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f98829])).
% 122.54/17.94 fof(f107016,definition,(
% 122.54/17.94 ![X0]: (sQ3080_spl <=> (~r1_tarski(k1_xboole_0,X0)))),
% 122.54/17.94 introduced(definition,[new_symbols(definition,[sQ3080_spl])],[split_symbol_definition])).
% 122.54/17.94 fof(f107017,plain,(
% 122.54/17.94 ![X0]: (~r1_tarski(k1_xboole_0,X0)|~sQ3080_spl)),
% 122.54/17.94 inference(component_clause,[status(thm)],[f107016])).
% 122.54/17.94 fof(f107020,plain,(
% 122.54/17.94 $false|~sQ3080_spl),
% 122.54/17.94 inference(forward_subsumption_resolution,[status(thm)],[f107017,f17139])).
% 122.54/17.94 fof(f107021,plain,(
% 122.54/17.94 ~sQ3080_spl),
% 122.54/17.94 inference(contradiction_clause,[status(thm)],[f107020])).
% 122.54/17.94 fof(f109283,plain,(
% 122.54/17.94 ~v2_cat_1(sK5420_skl)|~l1_cat_1(sK5420_skl)|~v1_xboole_0(k1_xboole_0)|~sQ1654_spl),
% 122.54/17.94 inference(paramodulation,[status(thm)],[f93485,f48833])).
% 122.54/17.94 fof(f109289,plain,(
% 122.54/17.94 ~sQ1361_spl|~sQ1362_spl|~sQ2243_spl|~sQ1654_spl),
% 122.54/17.94 inference(split_clause,[status(thm)],[f109283,f88947,f88950,f94241,f90708])).
% 122.54/17.94 fof(f109290,plain,(
% 122.54/17.94 $false),
% 124.14/18.19 inference(sat_refutation,[status(thm)],[f88958,f88960,f88967,f89140,f90196,f90681,f90714,f90717,f91203,f91716,f92220,f92705,f93510,f94247,f94249,f94678,f94742,f95655,f98745,f98762,f98779,f98796,f98813,f98830,f107021,f109289])).
% 124.14/18.19 % SZS output end CNFRefutation for theBenchmark.p
% 14.07/18.38 % Elapsed time: 17.978317 seconds
% 14.07/18.38 % CPU time: 123.780717 seconds
% 14.07/18.38 % Total memory used: 5.061 GB
% 14.07/18.38 % Net memory used: 4.993 GB
%------------------------------------------------------------------------------