%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT159+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:07:23 PM UTC 2026
% Result : Theorem 11.60s 1.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT159+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n004.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 04:35:37 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.41 % Drodi V4.1.1
% 11.60/1.95 % Refutation found
% 11.60/1.95 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.60/1.95 % SZS output start CNFRefutation for theBenchmark
% 11.60/1.95 fof(f13,axiom,(
% 11.60/1.95 (! [V_h_2,T_b,V_Fa_2,T_a] :( c_Finite__Set_Ofinite(T_a,V_Fa_2)=> c_Finite__Set_Ofinite(T_b,c_Set_Oimage(T_a,T_b,V_h_2,V_Fa_2)) ) )),
% 11.60/1.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.60/1.95 fof(f119,axiom,(
% 11.60/1.95 (! [V_A_2,T_a] :( c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Finite__Set_Ocard(T_a,V_A_2))<=> ( V_A_2 != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))& c_Finite__Set_Ofinite(T_a,V_A_2) ) ) )),
% 11.60/1.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.60/1.95 fof(f146,axiom,(
% 11.60/1.95 c_Orderings_Obot__class_Obot(tc_Nat_Onat) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
% 11.60/1.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.60/1.95 fof(f150,axiom,(
% 11.60/1.95 (! [V_A_2,V_x_2,T_a] :( c_member(T_a,V_x_2,V_A_2)<=> hBOOL(hAPP(V_A_2,V_x_2)) ) )),
% 11.60/1.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.60/1.95 fof(f173,axiom,(
% 11.60/1.95 (! [V_N_2] :( c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2)<=> (? [B_m] :(! [B_x] :( c_member(tc_Nat_Onat,B_x,V_N_2)=> c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_x,B_m) ) ))) )),
% 11.60/1.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.60/1.95 fof(f209,axiom,(
% 11.60/1.95 (! [T_b,T_a,V_x_2,V_f_2,V_b_2] :( V_b_2 = hAPP(V_f_2,V_x_2)=> c_member(T_a,V_b_2,c_Set_Oimage(T_b,T_a,V_f_2,c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_HOL_Obool)))) ) )),
% 11.60/1.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.60/1.95 fof(f243,axiom,(
% 11.60/1.95 (! [V_n] : ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(c_Nat_OSuc,V_n),V_n) )),
% 11.60/1.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.60/1.95 fof(f424,axiom,(
% 11.60/1.95 c_HOL_Obool_Obool__size(c_fTrue) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
% 11.60/1.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.60/1.95 fof(f425,axiom,(
% 11.60/1.95 c_Finite__Set_Ocard(tc_Product__Type_Ounit,c_Orderings_Otop__class_Otop(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool))) = c_Groups_Oone__class_Oone(tc_Nat_Onat) ),
% 11.60/1.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.60/1.95 fof(f430,axiom,(
% 11.60/1.95 (! [T_a] :( class_Rings_Olinordered__semidom(T_a)=> c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Groups_Oone__class_Oone(T_a)) ) )),
% 11.60/1.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.60/1.95 fof(f439,axiom,(
% 11.60/1.95 c_HOL_Obool_Obool__size(c_fFalse) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
% 11.60/1.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.60/1.95 fof(f505,axiom,(
% 11.60/1.95 class_Rings_Olinordered__semidom(tc_Nat_Onat) ),
% 11.60/1.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.60/1.95 fof(f574,plain,(
% 11.60/1.95 ![V_h_2,T_b,V_Fa_2,T_a]: (~c_Finite__Set_Ofinite(T_a,V_Fa_2)|c_Finite__Set_Ofinite(T_b,c_Set_Oimage(T_a,T_b,V_h_2,V_Fa_2)))),
% 11.60/1.95 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 11.60/1.95 fof(f575,plain,(
% 11.60/1.95 ![V_Fa_2,T_a]: (~c_Finite__Set_Ofinite(T_a,V_Fa_2)|(![V_h_2,T_b]: c_Finite__Set_Ofinite(T_b,c_Set_Oimage(T_a,T_b,V_h_2,V_Fa_2))))),
% 11.60/1.95 inference(miniscoping,[status(thm)],[f574])).
% 11.60/1.95 fof(f576,plain,(
% 11.60/1.95 ![X0,X1,X2,X3]: (~c_Finite__Set_Ofinite(X0,X1)|c_Finite__Set_Ofinite(X2,c_Set_Oimage(X0,X2,X3,X1)))),
% 11.60/1.95 inference(cnf_transformation,[status(thm)],[f575])).
% 11.60/1.95 fof(f930,plain,(
% 11.60/1.95 ![V_A_2,T_a]: ((~c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Finite__Set_Ocard(T_a,V_A_2))|(~V_A_2=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))&c_Finite__Set_Ofinite(T_a,V_A_2)))&(c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Finite__Set_Ocard(T_a,V_A_2))|(V_A_2=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))|~c_Finite__Set_Ofinite(T_a,V_A_2))))),
% 11.60/1.95 inference(NNF_transformation,[status(thm)],[f119])).
% 11.60/1.95 fof(f931,plain,(
% 11.60/1.95 (![V_A_2,T_a]: (~c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Finite__Set_Ocard(T_a,V_A_2))|(~V_A_2=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))&c_Finite__Set_Ofinite(T_a,V_A_2))))&(![V_A_2,T_a]: (c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Finite__Set_Ocard(T_a,V_A_2))|(V_A_2=c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool))|~c_Finite__Set_Ofinite(T_a,V_A_2))))),
% 11.60/1.95 inference(miniscoping,[status(thm)],[f930])).
% 11.60/1.95 fof(f933,plain,(
% 11.60/1.95 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),c_Finite__Set_Ocard(X0,X1))|c_Finite__Set_Ofinite(X0,X1))),
% 11.60/1.95 inference(cnf_transformation,[status(thm)],[f931])).
% 11.60/1.95 fof(f1013,plain,(
% 11.60/1.95 c_Orderings_Obot__class_Obot(tc_Nat_Onat)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 11.60/1.95 inference(cnf_transformation,[status(thm)],[f146])).
% 11.60/1.95 fof(f1026,plain,(
% 11.60/1.95 ![V_A_2,V_x_2,T_a]: ((~c_member(T_a,V_x_2,V_A_2)|hBOOL(hAPP(V_A_2,V_x_2)))&(c_member(T_a,V_x_2,V_A_2)|~hBOOL(hAPP(V_A_2,V_x_2))))),
% 11.60/1.95 inference(NNF_transformation,[status(thm)],[f150])).
% 11.60/1.95 fof(f1027,plain,(
% 11.60/1.95 (![V_A_2,V_x_2]: ((![T_a]: ~c_member(T_a,V_x_2,V_A_2))|hBOOL(hAPP(V_A_2,V_x_2))))&(![V_A_2,V_x_2]: ((![T_a]: c_member(T_a,V_x_2,V_A_2))|~hBOOL(hAPP(V_A_2,V_x_2))))),
% 11.60/1.95 inference(miniscoping,[status(thm)],[f1026])).
% 11.60/1.95 fof(f1028,plain,(
% 11.60/1.95 ![X0,X1,X2]: (~c_member(X0,X1,X2)|hBOOL(hAPP(X2,X1)))),
% 11.60/1.95 inference(cnf_transformation,[status(thm)],[f1027])).
% 11.60/1.95 fof(f1029,plain,(
% 11.60/1.95 ![X0,X1,X2]: (c_member(X0,X1,X2)|~hBOOL(hAPP(X2,X1)))),
% 11.60/1.95 inference(cnf_transformation,[status(thm)],[f1027])).
% 11.60/1.95 fof(f1098,plain,(
% 11.60/1.95 ![V_N_2]: (c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2)<=>(?[B_m]: ![B_x]: (~c_member(tc_Nat_Onat,B_x,V_N_2)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_x,B_m))))),
% 11.60/1.95 inference(pre_NNF_transformation,[status(thm)],[f173])).
% 11.60/1.95 fof(f1099,plain,(
% 11.60/1.95 ![V_N_2]: ((~c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2)|(?[B_m]: ![B_x]: (~c_member(tc_Nat_Onat,B_x,V_N_2)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_x,B_m))))&(c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2)|(![B_m]: ?[B_x]: (c_member(tc_Nat_Onat,B_x,V_N_2)&~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_x,B_m)))))),
% 11.60/1.95 inference(NNF_transformation,[status(thm)],[f1098])).
% 11.60/1.95 fof(f1100,plain,(
% 11.60/1.95 (![V_N_2]: (~c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2)|(?[B_m]: ![B_x]: (~c_member(tc_Nat_Onat,B_x,V_N_2)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_x,B_m)))))&(![V_N_2]: (c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2)|(![B_m]: ?[B_x]: (c_member(tc_Nat_Onat,B_x,V_N_2)&~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_x,B_m)))))),
% 11.60/1.95 inference(miniscoping,[status(thm)],[f1099])).
% 11.60/1.95 fof(f1101,plain,(
% 11.60/1.95 (![V_N_2]: (~c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2)|![B_x]: (~c_member(tc_Nat_Onat,B_x,V_N_2)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_x,sK13_skl(V_N_2)))))&(![V_N_2]: (c_Finite__Set_Ofinite(tc_Nat_Onat,V_N_2)|(![B_m]: (c_member(tc_Nat_Onat,sK14_skl(B_m,V_N_2),V_N_2)&~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK14_skl(B_m,V_N_2),B_m)))))),
% 11.60/1.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(B_m,sK13_skl(V_N_2)),skolemize(B_x,sK14_skl(B_m,V_N_2))],[f1100])).
% 11.60/1.95 fof(f1102,plain,(
% 11.60/1.95 ![X0,X1]: (~c_Finite__Set_Ofinite(tc_Nat_Onat,X0)|~c_member(tc_Nat_Onat,X1,X0)|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,sK13_skl(X0)))),
% 11.60/1.95 inference(cnf_transformation,[status(thm)],[f1101])).
% 11.60/1.95 fof(f1213,plain,(
% 11.60/1.95 ![T_b,T_a,V_x_2,V_f_2,V_b_2]: (~V_b_2=hAPP(V_f_2,V_x_2)|c_member(T_a,V_b_2,c_Set_Oimage(T_b,T_a,V_f_2,c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_HOL_Obool)))))),
% 11.60/1.95 inference(pre_NNF_transformation,[status(thm)],[f209])).
% 11.60/1.95 fof(f1214,plain,(
% 11.60/1.95 ![V_f_2,V_b_2]: ((![V_x_2]: ~V_b_2=hAPP(V_f_2,V_x_2))|(![T_b,T_a]: c_member(T_a,V_b_2,c_Set_Oimage(T_b,T_a,V_f_2,c_Orderings_Otop__class_Otop(tc_fun(T_b,tc_HOL_Obool))))))),
% 11.60/1.95 inference(miniscoping,[status(thm)],[f1213])).
% 11.60/1.95 fof(f1215,plain,(
% 11.60/1.95 ![X0,X1,X2,X3,X4]: (~X0=hAPP(X1,X2)|c_member(X3,X0,c_Set_Oimage(X4,X3,X1,c_Orderings_Otop__class_Otop(tc_fun(X4,tc_HOL_Obool)))))),
% 11.60/1.95 inference(cnf_transformation,[status(thm)],[f1214])).
% 11.60/1.95 fof(f1316,plain,(
% 11.60/1.95 ![X0]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(c_Nat_OSuc,X0),X0))),
% 11.60/1.95 inference(cnf_transformation,[status(thm)],[f243])).
% 11.60/1.95 fof(f1916,plain,(
% 11.60/1.95 c_HOL_Obool_Obool__size(c_fTrue)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 11.60/1.95 inference(cnf_transformation,[status(thm)],[f424])).
% 11.60/1.95 fof(f1917,plain,(
% 11.60/1.95 c_Finite__Set_Ocard(tc_Product__Type_Ounit,c_Orderings_Otop__class_Otop(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool)))=c_Groups_Oone__class_Oone(tc_Nat_Onat)),
% 11.60/1.96 inference(cnf_transformation,[status(thm)],[f425])).
% 11.60/1.96 fof(f1927,plain,(
% 11.60/1.96 ![T_a]: (~class_Rings_Olinordered__semidom(T_a)|c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Groups_Oone__class_Oone(T_a)))),
% 11.60/1.96 inference(pre_NNF_transformation,[status(thm)],[f430])).
% 11.60/1.96 fof(f1928,plain,(
% 11.60/1.96 ![X0]: (~class_Rings_Olinordered__semidom(X0)|c_Orderings_Oord__class_Oless(X0,c_Groups_Ozero__class_Ozero(X0),c_Groups_Oone__class_Oone(X0)))),
% 11.60/1.96 inference(cnf_transformation,[status(thm)],[f1927])).
% 11.60/1.96 fof(f1953,plain,(
% 11.60/1.96 c_HOL_Obool_Obool__size(c_fFalse)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
% 11.60/1.96 inference(cnf_transformation,[status(thm)],[f439])).
% 11.60/1.96 fof(f2147,plain,(
% 11.60/1.96 class_Rings_Olinordered__semidom(tc_Nat_Onat)),
% 11.60/1.96 inference(cnf_transformation,[status(thm)],[f505])).
% 11.60/1.96 fof(f2228,plain,(
% 11.60/1.96 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Orderings_Obot__class_Obot(tc_Nat_Onat),c_Finite__Set_Ocard(X0,X1))|c_Finite__Set_Ofinite(X0,X1))),
% 11.60/1.96 inference(backward_demodulation,[status(thm)],[f1013,f933])).
% 11.60/1.96 fof(f2276,plain,(
% 11.60/1.96 ![X0,X1,X2,X3]: (c_member(X0,hAPP(X1,X2),c_Set_Oimage(X3,X0,X1,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))))),
% 11.60/1.96 inference(destructive_equality_resolution,[status(thm)],[f1215])).
% 11.60/1.96 fof(f2426,plain,(
% 11.60/1.96 c_Orderings_Obot__class_Obot(tc_Nat_Onat)=c_HOL_Obool_Obool__size(c_fTrue)),
% 11.60/1.96 inference(backward_demodulation,[status(thm)],[f1916,f1013])).
% 11.60/1.96 fof(f2431,plain,(
% 11.60/1.96 c_HOL_Obool_Obool__size(c_fTrue)=c_HOL_Obool_Obool__size(c_fFalse)),
% 11.60/1.96 inference(backward_demodulation,[status(thm)],[f1953,f1916])).
% 11.60/1.96 fof(f2473,plain,(
% 11.60/1.96 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_HOL_Obool_Obool__size(c_fTrue),c_Finite__Set_Ocard(X0,X1))|c_Finite__Set_Ofinite(X0,X1))),
% 11.60/1.96 inference(backward_demodulation,[status(thm)],[f2426,f2228])).
% 11.60/1.96 fof(f2540,plain,(
% 11.60/1.96 ![X0,X1]: (~c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_HOL_Obool_Obool__size(c_fFalse),c_Finite__Set_Ocard(X0,X1))|c_Finite__Set_Ofinite(X0,X1))),
% 11.60/1.96 inference(forward_demodulation,[status(thm)],[f2431,f2473])).
% 11.60/1.96 fof(f2694,plain,(
% 11.60/1.96 ![X0,X1,X2,X3]: (c_member(X0,X1,X2)|~c_member(X3,X1,X2))),
% 11.60/1.96 inference(resolution,[status(thm)],[f1029,f1028])).
% 11.60/1.96 fof(f2795,plain,(
% 11.60/1.96 ~class_Rings_Olinordered__semidom(tc_Nat_Onat)|c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_HOL_Obool_Obool__size(c_fFalse),c_Groups_Oone__class_Oone(tc_Nat_Onat))),
% 11.60/1.96 inference(paramodulation,[status(thm)],[f1953,f1928])).
% 11.60/1.96 fof(f2796,plain,(
% 11.60/1.96 c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_HOL_Obool_Obool__size(c_fFalse),c_Groups_Oone__class_Oone(tc_Nat_Onat))),
% 11.60/1.96 inference(forward_subsumption_resolution,[status(thm)],[f2795,f2147])).
% 11.60/1.96 fof(f4123,plain,(
% 11.60/1.96 ~c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_HOL_Obool_Obool__size(c_fFalse),c_Groups_Oone__class_Oone(tc_Nat_Onat))|c_Finite__Set_Ofinite(tc_Product__Type_Ounit,c_Orderings_Otop__class_Otop(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool)))),
% 11.60/1.96 inference(paramodulation,[status(thm)],[f1917,f2540])).
% 11.60/1.96 fof(f4128,plain,(
% 11.60/1.96 c_Finite__Set_Ofinite(tc_Product__Type_Ounit,c_Orderings_Otop__class_Otop(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool)))),
% 11.60/1.96 inference(forward_subsumption_resolution,[status(thm)],[f4123,f2796])).
% 11.60/1.96 fof(f5043,plain,(
% 11.60/1.96 ![X0]: (~c_Finite__Set_Ofinite(tc_Nat_Onat,X0)|~c_member(tc_Nat_Onat,hAPP(c_Nat_OSuc,sK13_skl(X0)),X0))),
% 11.60/1.96 inference(resolution,[status(thm)],[f1102,f1316])).
% 11.60/1.96 fof(f6644,plain,(
% 11.60/1.96 ![X0,X1]: (~c_Finite__Set_Ofinite(tc_Nat_Onat,X0)|~c_member(X1,hAPP(c_Nat_OSuc,sK13_skl(X0)),X0))),
% 11.60/1.96 inference(resolution,[status(thm)],[f5043,f2694])).
% 11.60/1.96 fof(f6671,plain,(
% 11.60/1.96 ![X0,X1]: (~c_Finite__Set_Ofinite(tc_Nat_Onat,c_Set_Oimage(X0,X1,c_Nat_OSuc,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)))))),
% 11.60/1.96 inference(resolution,[status(thm)],[f6644,f2276])).
% 11.60/1.96 fof(f7165,plain,(
% 11.60/1.96 ![X0]: (~c_Finite__Set_Ofinite(X0,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool))))),
% 11.60/1.96 inference(resolution,[status(thm)],[f6671,f576])).
% 11.60/1.96 fof(f7177,plain,(
% 11.60/1.96 $false),
% 11.60/1.96 inference(backward_subsumption_resolution,[status(thm)],[f4128,f7165])).
% 11.60/1.96 % SZS output end CNFRefutation for theBenchmark.p
% 0.56/2.00 % Elapsed time: 1.615913 seconds
% 0.56/2.00 % CPU time: 12.322689 seconds
% 0.56/2.00 % Total memory used: 354.271 MB
% 0.56/2.00 % Net memory used: 343.365 MB
%------------------------------------------------------------------------------